http://us2.metamath.org:8888/mpeuni/mmrecent.html Recent proofs for Metamath proof system en http://us2.metamath.org:8888/mpeuni/nfeqf2.html 20-Jul-2022ax-12 2197. (Revised by Wolf Lammen, 20-Jul-2022.)
   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
    ]]> http://us2.metamath.org:8888/mpeuni/lshpne0.html 19-Jul-2022   ⊢ 𝑉 = (Base‘𝑊)    &
   ⊢ 𝑁 = (LSpan‘𝑊)    &
   ⊢ ⊕ = (LSSum‘𝑊)    &
   ⊢ 𝐻 = (LSHyp‘𝑊)    &
   ⊢ 0 = (0_g‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LMod)    &
   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &
   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &
   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒
   ⊢ (𝜑 → 𝑋 ≠ 0 )
    ]]> http://us2.metamath.org:8888/mpeuni/lvecindp.html 19-Jul-2022   ⊢ 𝑉 = (Base‘𝑊)    &
   ⊢ + = (+_g‘𝑊)    &
   ⊢ 𝐹 = (Scalar‘𝑊)    &
   ⊢ 𝐾 = (Base‘𝐹)    &
   ⊢ · = ( ·_𝑠 ‘𝑊)    &
   ⊢ 𝑆 = (LSubSp‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LVec)    &
   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &
   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &
   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &
   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &
   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &
   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &
   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &
   ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝑌) = ((𝐵 · 𝑋) + 𝑍))    ⇒
   ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝑌 = 𝑍))
    ]]> http://us2.metamath.org:8888/mpeuni/lssneln0.html 19-Jul-2022   ⊢ 0 = (0_g‘𝑊)    &
   ⊢ 𝑆 = (LSubSp‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LMod)    &
   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &
   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &
   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒
   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
    ]]> http://us2.metamath.org:8888/mpeuni/lssvneln0.html 19-Jul-2022   ⊢ 0 = (0_g‘𝑊)    &
   ⊢ 𝑆 = (LSubSp‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LMod)    &
   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &
   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒
   ⊢ (𝜑 → 𝑋 ≠ 0 )
    ]]> http://us2.metamath.org:8888/mpeuni/hashmap.html 18-Jul-2022   ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ↑_𝑚 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))
    ]]> http://us2.metamath.org:8888/mpeuni/pwxpndom2.html 18-Jul-2022   ⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 +_𝑐 (𝐴 × 𝐴)))
    ]]> http://us2.metamath.org:8888/mpeuni/ackbij1lem5.html 18-Jul-2022ackbij2 9269. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.)
   ⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +_𝑜 (card‘𝒫 𝐴)))
    ]]> http://us2.metamath.org:8888/mpeuni/wfrlem4.html 18-Jul-2022   ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}    ⇒
   ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
    ]]> http://us2.metamath.org:8888/mpeuni/opelxpii.html 17-Jul-2022   ⊢ 𝐴 ∈ 𝐶    &
   ⊢ 𝐵 ∈ 𝐷    ⇒
   ⊢ ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷)
    ]]> http://us2.metamath.org:8888/mpeuni/elpwbi.html 17-Jul-2022   ⊢ 𝐵 ∈ V    ⇒
   ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵)
    ]]> http://us2.metamath.org:8888/mpeuni/xppss12.html 17-Jul-2022   ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷))
    ]]> http://us2.metamath.org:8888/mpeuni/psspwb.html 17-Jul-2022   ⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵)
    ]]> http://us2.metamath.org:8888/mpeuni/pssn0.html 17-Jul-2022   ⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅)
    ]]> http://us2.metamath.org:8888/mpeuni/pssexg.html 17-Jul-2022   ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
    ]]> http://us2.metamath.org:8888/mpeuni/jaodd.html 17-Jul-2022jaoi 391. (Contributed by Steven Nguyen, 17-Jul-2022.)
   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &
   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃)))    ⇒
   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃)))
    ]]> http://us2.metamath.org:8888/mpeuni/ioin9i8.html 17-Jul-2022   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    &
   ⊢ (𝜒 → ¬ 𝜃)    &
   ⊢ (𝜓 → 𝜃)    ⇒
   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
    ]]> http://us2.metamath.org:8888/mpeuni/mapdom3.html 17-Jul-2022   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 ↑_𝑚 𝐵))
    ]]> http://us2.metamath.org:8888/mpeuni/map2xp.html 17-Jul-2022   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑_𝑚 2_𝑜) ≈ (𝐴 × 𝐴))
    ]]> http://us2.metamath.org:8888/mpeuni/map1.html 17-Jul-2022Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.)
   ⊢ (𝐴 ∈ 𝑉 → (1_𝑜 ↑_𝑚 𝐴) ≈ 1_𝑜)
    ]]> http://us2.metamath.org:8888/mpeuni/snmapen1.html 17-Jul-2022   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} ↑_𝑚 𝐵) ≈ 1_𝑜)
    ]]> http://us2.metamath.org:8888/mpeuni/snmapen.html 17-Jul-2022   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} ↑_𝑚 𝐵) ≈ {𝐴})
    ]]> http://us2.metamath.org:8888/mpeuni/mapsnen.html 17-Jul-2022Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.) (Proof shortened by AV, 17-Jul-2022.)
   ⊢ 𝐴 ∈ V    &
   ⊢ 𝐵 ∈ V    ⇒
   ⊢ (𝐴 ↑_𝑚 {𝐵}) ≈ 𝐴
    ]]> http://us2.metamath.org:8888/mpeuni/mapsn.html 17-Jul-2022Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.)
   ⊢ 𝐴 ∈ V    &
   ⊢ 𝐵 ∈ V    ⇒
   ⊢ (𝐴 ↑_𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
    ]]> http://us2.metamath.org:8888/mpeuni/iedgvalsnop.html 15-Jul-2022   ⊢ 𝐵 ∈ V    &
   ⊢ 𝐺 = {⟨𝐵, 𝐵⟩}    ⇒
   ⊢ (iEdg‘𝐺) = {𝐵}
    ]]> http://us2.metamath.org:8888/mpeuni/vtxvalsnop.html 15-Jul-2022   ⊢ 𝐵 ∈ V    &
   ⊢ 𝐺 = {⟨𝐵, 𝐵⟩}    ⇒
   ⊢ (Vtx‘𝐺) = {𝐵}
    ]]> http://us2.metamath.org:8888/mpeuni/snopeqopsnid.html 15-Jul-2022   ⊢ 𝐴 ∈ V    ⇒
   ⊢ {⟨𝐴, 𝐴⟩} = ⟨{𝐴}, {𝐴}⟩
    ]]> http://us2.metamath.org:8888/mpeuni/snopeqop.html 15-Jul-2022   ⊢ 𝐴 ∈ V    &
   ⊢ 𝐵 ∈ V    ⇒
   ⊢ ({⟨𝐴, 𝐵⟩} = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = {𝐴}))
    ]]> http://us2.metamath.org:8888/mpeuni/opeqsn.html 15-Jul-2022   ⊢ 𝐴 ∈ V    &
   ⊢ 𝐵 ∈ V    ⇒
   ⊢ (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))
    ]]> http://us2.metamath.org:8888/mpeuni/opeqsng.html 15-Jul-2022   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})))
    ]]> http://us2.metamath.org:8888/mpeuni/map0e.html 14-Jul-2022Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 14-Jul-2022.)
   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑_𝑚 ∅) = 1_𝑜)
    ]]> http://us2.metamath.org:8888/mpeuni/lspsncv0.html 13-Jul-2022PtakPulmannova] p. 68 for "covers".) (Contributed by NM, 12-Aug-2014.) (Revised by AV, 13-Jul-2022.)
   ⊢ 𝑉 = (Base‘𝑊)    &
   ⊢ 0 = (0_g‘𝑊)    &
   ⊢ 𝑆 = (LSubSp‘𝑊)    &
   ⊢ 𝑁 = (LSpan‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LVec)    &
   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒
   ⊢ (𝜑 → ¬ ∃𝑦 ∈ 𝑆 ({ 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ (𝑁‘{𝑋})))
    ]]> http://us2.metamath.org:8888/mpeuni/lssssr.html 13-Jul-2022ssrdv 3743 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.)
   ⊢ 0 = (0_g‘𝑊)    &
   ⊢ 𝑆 = (LSubSp‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LMod)    &
   ⊢ (𝜑 → 𝑇 ⊆ 𝑉)    &
   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &
   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈))    ⇒
   ⊢ (𝜑 → 𝑇 ⊆ 𝑈)
    ]]> http://us2.metamath.org:8888/mpeuni/uzind4i.html 13-Jul-2022uzind4 11951 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ_≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 11896). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.)
   ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓))    &
   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒))    &
   ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &
   ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏))    &
   ⊢ 𝜓    &
   ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝜒 → 𝜃))    ⇒
   ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝜏)
    ]]> http://us2.metamath.org:8888/mpeuni/nf5dv.html 13-Jul-2022df-nf 1852 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 13-Jul-2022.)
   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒
   ⊢ (𝜑 → Ⅎ𝑥𝜓)
    ]]> http://us2.metamath.org:8888/mpeuni/lspfixed.html 12-Jul-2022   ⊢ 𝑉 = (Base‘𝑊)    &
   ⊢ + = (+_g‘𝑊)    &
   ⊢ 0 = (0_g‘𝑊)    &
   ⊢ 𝑁 = (LSpan‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ LVec)    &
   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &
   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &
   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    &
   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍}))    &
   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒
   ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))
    ]]> http://us2.metamath.org:8888/mpeuni/karden.html 12-Jul-2022carden 9577). The hypotheses correspond to the definition of kard of [Enderton] p. 222 (which we don't define separately since currently we do not use it elsewhere). This theorem along with kardex 8923 justify the definition of kard. The restriction to the least rank prevents the proper class that would result from {𝑥 ∣ 𝑥 ≈ 𝐴}. (Contributed by NM, 18-Dec-2003.) (Revised by AV, 12-Jul-2022.)
   ⊢ 𝐴 ∈ V    &
   ⊢ 𝐶 = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}    &
   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}    ⇒
   ⊢ (𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵)
    ]]> http://us2.metamath.org:8888/mpeuni/brecop2.html 12-Jul-2022   ⊢ dom ∼ = (𝐺 × 𝐺)    &
   ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ )    &
   ⊢ 𝑅 ⊆ (𝐻 × 𝐻)    &
   ⊢ ≤ ⊆ (𝐺 × 𝐺)    &
   ⊢ ¬ ∅ ∈ 𝐺    &
   ⊢ dom + = (𝐺 × 𝐺)    &
   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶)))    ⇒
   ⊢ ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶))
    ]]> http://us2.metamath.org:8888/mpeuni/alcomiw.html 12-Jul-2022alcom 2187. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)
   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒
   ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
    ]]> http://us2.metamath.org:8888/mpeuni/equvelv.html 12-Jul-2022equvel 2481 with distinct variable restrictions and fewer axiom usage. (Contributed by Wolf Lammen, 10-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)
   ⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦))
    ]]> http://us2.metamath.org:8888/mpeuni/equvinv.html 12-Jul-2022Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2168, ax-13 2396. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable (𝑧) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)
   ⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦))
    ]]> http://us2.metamath.org:8888/mpeuni/oexpnegALTV.html 10-Jul-2022   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁))
    ]]> http://us2.metamath.org:8888/mpeuni/pjhthlem1.html 10-Jul-2022pjhth 28593. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (Proof shortened by AV, 10-Jul-2022.) (New usage is discouraged.)
   ⊢ 𝐻 ∈ C_ℋ    &
   ⊢ (𝜑 → 𝐴 ∈ ℋ)    &
   ⊢ (𝜑 → 𝐵 ∈ 𝐻)    &
   ⊢ (𝜑 → 𝐶 ∈ 𝐻)    &
   ⊢ (𝜑 → ∀𝑥 ∈ 𝐻 (norm_ℎ‘(𝐴 −_ℎ 𝐵)) ≤ (norm_ℎ‘(𝐴 −_ℎ 𝑥)))    &
   ⊢ 𝑇 = (((𝐴 −_ℎ 𝐵) ·_ih 𝐶) / ((𝐶 ·_ih 𝐶) + 1))    ⇒
   ⊢ (𝜑 → ((𝐴 −_ℎ 𝐵) ·_ih 𝐶) = 0)
    ]]> http://us2.metamath.org:8888/mpeuni/nvge0.html 10-Jul-2022Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Proof shortened by AV, 10-Jul-2022.) (New usage is discouraged.)
   ⊢ 𝑋 = (BaseSet‘𝑈)    &
   ⊢ 𝑁 = (norm_CV‘𝑈)    ⇒
   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝑁‘𝐴))
    ]]> http://us2.metamath.org:8888/mpeuni/pjthlem1.html 10-Jul-2022pjth 23437. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) (Proof shortened by AV, 10-Jul-2022.)
   ⊢ 𝑉 = (Base‘𝑊)    &
   ⊢ 𝑁 = (norm‘𝑊)    &
   ⊢ + = (+_g‘𝑊)    &
   ⊢ − = (-_g‘𝑊)    &
   ⊢ , = (·_𝑖‘𝑊)    &
   ⊢ 𝐿 = (LSubSp‘𝑊)    &
   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &
   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &
   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &
   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &
   ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑁‘𝐴) ≤ (𝑁‘(𝐴 − 𝑥)))    &
   ⊢ 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))    ⇒
   ⊢ (𝜑 → (𝐴 , 𝐵) = 0)
    ]]> http://us2.metamath.org:8888/mpeuni/prmgaplem7.html 10-Jul-2022prmgap 15978. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.)
   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &
   ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑_𝑚 ℕ))    &
   ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))    ⇒
   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
    ]]> http://us2.metamath.org:8888/mpeuni/iserodd.html 10-Jul-2022   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐶 ∈ ℂ)    &
   ⊢ (𝑛 = ((2 · 𝑘) + 1) → 𝐵 = 𝐶)    ⇒
   ⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ₀ ↦ 𝐶)) ⇝ 𝐴 ↔ seq1( + , (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))) ⇝ 𝐴))
    ]]> http://us2.metamath.org:8888/mpeuni/oddprm.html 10-Jul-2022   ⊢ (𝑁 ∈ (ℙ ∖ {2}) → ((𝑁 − 1) / 2) ∈ ℕ)
    ]]> http://us2.metamath.org:8888/mpeuni/flodddiv4t2lthalf.html 10-Jul-2022   ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → ((⌊‘(𝑁 / 4)) · 2) < (𝑁 / 2))
    ]]> http://us2.metamath.org:8888/mpeuni/nn0oddm1d2.html 10-Jul-2022   ⊢ (𝑁 ∈ ℕ₀ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℕ₀))
    ]]> http://us2.metamath.org:8888/mpeuni/nno.html 10-Jul-2022   ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → ((𝑁 − 1) / 2) ∈ ℕ)
    ]]> http://us2.metamath.org:8888/mpeuni/nn0ehalf.html 10-Jul-2022   ⊢ ((𝑁 ∈ ℕ₀ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ₀)
    ]]> http://us2.metamath.org:8888/mpeuni/evennn02n.html 10-Jul-2022   ⊢ (𝑁 ∈ ℕ₀ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ₀ (2 · 𝑛) = 𝑁))
    ]]> http://us2.metamath.org:8888/mpeuni/oexpneg.html 10-Jul-2022   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁))
    ]]> http://us2.metamath.org:8888/mpeuni/climcnds.html 10-Jul-202202↑𝑛 · 𝑎(2↑𝑛) converges. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.)
   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ)    &
   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘))    &
   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &
   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))    ⇒
   ⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq0( + , 𝐺) ∈ dom ⇝ ))
    ]]> http://us2.metamath.org:8888/mpeuni/climcndslem2.html 10-Jul-2022climcnds 14796: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.)
   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ)    &
   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘))    &
   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &
   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))    ⇒
   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))
    ]]> http://us2.metamath.org:8888/mpeuni/2tnp1ge0ge0.html 10-Jul-2022   ⊢ (𝑁 ∈ ℤ → (0 ≤ ((2 · 𝑁) + 1) ↔ 0 ≤ 𝑁))
    ]]> http://us2.metamath.org:8888/mpeuni/nfimd.html 10-Jul-2022nfim 1971. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1852 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1968. (Revised by Wolf Lammen, 10-Jul-2022.)
   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &
   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒
   ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
    ]]> http://us2.metamath.org:8888/mpeuni/oddge22np1.html 9-Jul-2022   ⊢ (𝑁 ∈ (ℤ_≥‘2) → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ ((2 · 𝑛) + 1) = 𝑁))
    ]]> http://us2.metamath.org:8888/mpeuni/efcllem.html 9-Jul-2022efcl 15026. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 14828 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) (Proof shortened by AV, 9-Jul-2022.)
   ⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒
   ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )
    ]]> http://us2.metamath.org:8888/mpeuni/geoihalfsum.html 9-Jul-2022geoisum1 14823. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 14825 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by AV, 9-Jul-2022.)
   ⊢ Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1
    ]]> http://us2.metamath.org:8888/mpeuni/iseralt.html 9-Jul-2022isermulc2 14601.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.)
   ⊢ 𝑍 = (ℤ_≥‘𝑀)    &
   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &
   ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)    &
   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))    &
   ⊢ (𝜑 → 𝐺 ⇝ 0)    &
   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))    ⇒
   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
    ]]> http://us2.metamath.org:8888/mpeuni/amgm2.html 9-Jul-2022   ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2))
    ]]> http://us2.metamath.org:8888/mpeuni/sqrlem7.html 9-Jul-202201sqrex 14203. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.)
   ⊢ 𝑆 = {𝑥 ∈ ℝ⁺ ∣ (𝑥↑2) ≤ 𝐴}    &
   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &
   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒
   ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴)
    ]]> http://us2.metamath.org:8888/mpeuni/2swrd2eqwrdeq.html 9-Jul-2022   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 substr ⟨0, ((♯‘𝑊) − 2)⟩) = (𝑈 substr ⟨0, ((♯‘𝑊) − 2)⟩) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))))
    ]]> http://us2.metamath.org:8888/mpeuni/fldiv4lem1div2uz2.html 9-Jul-2022   ⊢ (𝑁 ∈ (ℤ_≥‘2) → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2))
    ]]> http://us2.metamath.org:8888/mpeuni/prodge0ld.html 9-Jul-2022   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &
   ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)    &
   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))    ⇒
   ⊢ (𝜑 → 0 ≤ 𝐴)
    ]]> http://us2.metamath.org:8888/mpeuni/prodge0rd.html 9-Jul-2022   ⊢ (𝜑 → 𝐴 ∈ ℝ⁺)    &
   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &
   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))    ⇒
   ⊢ (𝜑 → 0 ≤ 𝐵)
    ]]> http://us2.metamath.org:8888/mpeuni/zgt1rpn0n1.html 9-Jul-2022   ⊢ (𝐵 ∈ (ℤ_≥‘2) → (𝐵 ∈ ℝ⁺ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1))
    ]]> http://us2.metamath.org:8888/mpeuni/19.38b.html 9-Jul-202219.38 1908 can be strengthened to an equivalence. See also 19.38a 1909. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)
   ⊢ (Ⅎ𝑥𝜓 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
    ]]> http://us2.metamath.org:8888/mpeuni/19.38a.html 9-Jul-202219.38 1908 can be strengthened to an equivalence. See also 19.38b 1911. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)
   ⊢ (Ⅎ𝑥𝜑 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
    ]]> http://us2.metamath.org:8888/mpeuni/axc7e.html 8-Jul-2022axc7 2283 using the existential quantifier. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
   ⊢ (∃𝑥∀𝑥𝜑 → 𝜑)
    ]]> http://us2.metamath.org:8888/mpeuni/equsalhw.html 8-Jul-2022equsalh 2437 with a dv condition which does not require ax-13 2396. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
   ⊢ (𝜓 → ∀𝑥𝜓)    &
   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒
   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
    ]]> http://us2.metamath.org:8888/mpeuni/19.9d.html 8-Jul-202219.9 2222. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) df-nf 1852 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
   ⊢ (𝜓 → Ⅎ𝑥𝜑)    ⇒
   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
    ]]> http://us2.metamath.org:8888/mpeuni/numclwwlkqhash.html 7-Jul-2022   ⊢ 𝑉 = (Vtx‘𝐺)    &
   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    ⇒
   ⊢ (((𝐺RegUSGraph𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (♯‘(𝑋𝑄𝑁)) = ((𝐾↑𝑁) − (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁))))
    ]]> http://us2.metamath.org:8888/mpeuni/clwwlkvbij.html 7-Jul-2022   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁))
    ]]> http://us2.metamath.org:8888/mpeuni/uhgrwkspth.html 7-Jul-2022   ⊢ ((𝐺 ∈ 𝑊 ∧ (♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
    ]]> http://us2.metamath.org:8888/mpeuni/nfan1.html 7-Jul-2022nfan 1974. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1852 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)
   ⊢ Ⅎ𝑥𝜑    &
   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒
   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
    ]]> http://us2.metamath.org:8888/mpeuni/edgnbusgreu.html 6-Jul-2022   ⊢ 𝐸 = (Edg‘𝐺)    &
   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑀)    ⇒
   ⊢ (((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑉) ∧ (𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶)) → ∃!𝑛 ∈ 𝑁 𝐶 = {𝑀, 𝑛})
    ]]> http://us2.metamath.org:8888/mpeuni/ushgredgedgloop.html 6-Jul-2022   ⊢ 𝐸 = (Edg‘𝐺)    &
   ⊢ 𝐼 = (iEdg‘𝐺)    &
   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}    &
   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑁}}    &
   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒
   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
    ]]> http://us2.metamath.org:8888/mpeuni/uhgrvtxedgiedgb.html 6-Jul-2022   ⊢ 𝐼 = (iEdg‘𝐺)    &
   ⊢ 𝐸 = (Edg‘𝐺)    ⇒
   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → (∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖) ↔ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒))
    ]]> http://us2.metamath.org:8888/mpeuni/toponrestid.html 6-Jul-2022   ⊢ 𝐴 ∈ (TopOn‘𝐵)    ⇒
   ⊢ 𝐴 = (𝐴 ↾_t 𝐵)
    ]]> http://us2.metamath.org:8888/mpeuni/nfimt.html 6-Jul-2022nfim 1971 and nfimd 1967. (Contributed by BJ, 20-Oct-2021.) Eliminate curried form, former name nfimt2. (Revised by Wolf Lammen, 6-Jul-2022.)
   ⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
    ]]> http://us2.metamath.org:8888/mpeuni/distspace.html 5-Jul-2022distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set 𝑋 equipped with a distance 𝐷, which is a mapping of two elements of the base set to the (extended) reals and which is non-negative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐷:(𝑋 × 𝑋)⟶ℝ^* ∧ (𝐴𝐷𝐴) = 0) ∧ (0 ≤ (𝐴𝐷𝐵) ∧ (𝐴𝐷𝐵) = (𝐵𝐷𝐴))))
    ]]> http://us2.metamath.org:8888/mpeuni/chmaidscmat.html 5-Jul-2022   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &
   ⊢ 𝐵 = (Base‘𝐴)    &
   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &
   ⊢ 𝑃 = (Poly₁‘𝑅)    &
   ⊢ 𝐸 = (Base‘𝑃)    &
   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &
   ⊢ 𝐾 = (Base‘𝑌)    &
   ⊢ · = ( ·_𝑠 ‘𝑌)    &
   ⊢ 1 = (1_r‘𝑌)    &
   ⊢ 𝑆 = (𝑁 ScMat 𝑃)    ⇒
   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐶‘𝑀) · 1 ) ∈ 𝑆)
    ]]> http://us2.metamath.org:8888/mpeuni/cramerimplem1.html 5-Jul-2022cramerimp 20720: The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 5-Jul-2022.)
   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &
   ⊢ 𝑉 = ((Base‘𝑅) ↑_𝑚 𝑁)    &
   ⊢ 𝐸 = (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)    &
   ⊢ 𝐷 = (𝑁 maDet 𝑅)    ⇒
   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼))
    ]]> http://us2.metamath.org:8888/mpeuni/copsgndif.html 5-Jul-2022   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &
   ⊢ 𝑆 = (pmSgn‘𝑁)    &
   ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾}))    ⇒
   ⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → ((𝑌 ∘ 𝑍)‘(𝑄 ↾ (𝑁 ∖ {𝐾}))) = ((𝑌 ∘ 𝑆)‘𝑄)))
    ]]> http://us2.metamath.org:8888/mpeuni/minmar1marrep.html 4-Jul-2022   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &
   ⊢ 𝐵 = (Base‘𝐴)    &
   ⊢ 1 = (1_r‘𝑅)    ⇒
   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 minMatR1 𝑅)‘𝑀) = (𝑀(𝑁 matRRep 𝑅) 1 ))
    ]]> http://us2.metamath.org:8888/mpeuni/djuunxp.html 4-Jul-2022   ⊢ ((𝐴 ⊔ 𝐵) ∪ (𝐵 ⊔ 𝐴)) = ({∅, 1_𝑜} × (𝐴 ∪ 𝐵))
    ]]> http://us2.metamath.org:8888/mpeuni/pmatcollpwfi.html 3-Jul-2022   ⊢ 𝑃 = (Poly₁‘𝑅)    &
   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &
   ⊢ 𝐵 = (Base‘𝐶)    &
   ⊢ ∗ = ( ·_𝑠 ‘𝐶)    &
   ⊢ ↑ = (._g‘(mulGrp‘𝑃))    &
   ⊢ 𝑋 = (var₁‘𝑅)    &
   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒
   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ₀ 𝑀 = (𝐶 Σ_g (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))))
    ]]> http://us2.metamath.org:8888/mpeuni/mdet0.html 3-Jul-2022   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &
   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &
   ⊢ 𝑍 = (0_g‘𝐴)    &
   ⊢ 0 = (0_g‘𝑅)    ⇒
   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅) → (𝐷‘𝑍) = 0 )
    ]]> http://us2.metamath.org:8888/mpeuni/matmulcell.html 3-Jul-2022   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &
   ⊢ 𝐵 = (Base‘𝐴)    &
   ⊢ × = (._r‘𝐴)    ⇒
   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 × 𝑌)𝐽) = (𝑅 Σ_g (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗)(._r‘𝑅)(𝑗𝑌𝐽)))))
    ]]> http://us2.metamath.org:8888/mpeuni/mpt2frlmd.html 3-Jul-2022   ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑀))    &
   ⊢ 𝑉 = (Base‘𝐹)    &
   ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → 𝐴 = 𝐵)    &
   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑀) → 𝐴 ∈ 𝑋)    &
   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑀) → 𝐵 ∈ 𝑌)    &
   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ 𝑀 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉))    ⇒
   ⊢ (𝜑 → (𝑍 = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑀 ↦ 𝐵) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑀 (𝑖𝑍𝑗) = 𝐴))
    ]]> http://us2.metamath.org:8888/mpeuni/zrhcopsgnelbas.html 3-Jul-2022   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &
   ⊢ 𝑆 = (pmSgn‘𝑁)    &
   ⊢ 𝑌 = (ℤRHom‘𝑅)    ⇒
   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅))
    ]]> http://us2.metamath.org:8888/mpeuni/cofipsgn.html 3-Jul-2022   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &
   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒
   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑄) = (𝑌‘(𝑆‘𝑄)))
    ]]> http://us2.metamath.org:8888/mpeuni/gsummptnn0fz.html 3-Jul-2022   ⊢ 𝐵 = (Base‘𝐺)    &
   ⊢ 0 = (0_g‘𝐺)    &
   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &
   ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ 𝐶 ∈ 𝐵)    &
   ⊢ (𝜑 → 𝑆 ∈ ℕ₀)    &
   ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ (𝑆 < 𝑘 → 𝐶 = 0 ))    ⇒
   ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ ℕ₀ ↦ 𝐶)) = (𝐺 Σ_g (𝑘 ∈ (0...𝑆) ↦ 𝐶)))
    ]]> http://us2.metamath.org:8888/mpeuni/estrres.html 3-Jul-2022   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})    &
   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &
   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &
   ⊢ (𝜑 → · ∈ 𝑌)    &
   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &
   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒
   ⊢ (𝜑 → ((𝐶 ↾_s 𝐴) sSet ⟨(Hom ‘ndx), 𝐺⟩) = {⟨(Base‘ndx), 𝐴⟩, ⟨(Hom ‘ndx), 𝐺⟩, ⟨(comp‘ndx), · ⟩})
    ]]> http://us2.metamath.org:8888/mpeuni/inveq.html 3-Jul-2022Adamek] p. 28. (Contributed by AV, 10-Apr-2020.) (Revised by AV, 3-Jul-2022.)
   ⊢ 𝐵 = (Base‘𝐶)    &
   ⊢ 𝑁 = (Inv‘𝐶)    &
   ⊢ (𝜑 → 𝐶 ∈ Cat)    &
   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &
   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒
   ⊢ (𝜑 → ((𝐹(𝑋𝑁𝑌)𝐺 ∧ 𝐹(𝑋𝑁𝑌)𝐾) → 𝐺 = 𝐾))
    ]]> http://us2.metamath.org:8888/mpeuni/ressval3d.html 3-Jul-2022   ⊢ 𝑅 = (𝑆 ↾_s 𝐴)    &
   ⊢ 𝐵 = (Base‘𝑆)    &
   ⊢ 𝐸 = (Base‘ndx)    &
   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &
   ⊢ (𝜑 → Fun 𝑆)    &
   ⊢ (𝜑 → 𝐸 ∈ dom 𝑆)    &
   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒
   ⊢ (𝜑 → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
    ]]> http://us2.metamath.org:8888/mpeuni/fnmpt2ovd.html 3-Jul-2022   ⊢ (𝜑 → 𝑀 Fn (𝐴 × 𝐵))    &
   ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → 𝐷 = 𝐶)    &
   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) → 𝐷 ∈ 𝑈)    &
   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒
   ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐵 (𝑖𝑀𝑗) = 𝐷))]]>