P. 206 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20501-20600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cpmadugsumfi 20501*	The product of the characteristic matrix of a given matrix and its adjunct represented as finite sum. (Contributed by AV, 7-Nov-2019.) (Proof shortened by AV, 29-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ × = (.r‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐼 × (𝐽‘𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))))
Theorem	cpmadugsum 20502*	The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite sum. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ × = (.r‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐼 × (𝐽‘𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))))
Theorem	cpmidgsum2 20503*	Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ × = (.r‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (𝐶‘𝑀)    &   ⊢ 𝐻 = (𝐾 · 1 )    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))))
Theorem	cpmidg2sum 20504*	Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ × = (.r‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (𝐶‘𝑀)    &   ⊢ 𝑈 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))))
Theorem	cpmadumatpolylem1 20505*	Lemma 1 for cpmadumatpoly 20507. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑍 = (var1‘𝑅)    &   ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    ⇒   ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚 ℕ0))
Theorem	cpmadumatpolylem2 20506*	Lemma 2 for cpmadumatpoly 20507. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑍 = (var1‘𝑅)    &   ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    ⇒   ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑈 ∘ 𝐺) finSupp (0g‘𝐴))
Theorem	cpmadumatpoly 20507*	The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 7-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑍 = (var1‘𝑅)    &   ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀))    &   ⊢ 𝐽 = (𝑁 maAdju 𝑃)    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐼‘(𝐷 × (𝐽‘𝐷))) = (𝑄 Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛)) ∗ (𝑛 ↑ 𝑋)))))
Theorem	cayhamlem2 20508	Lemma for cayhamlem3 20511. (Contributed by AV, 24-Nov-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    &   ⊢ · = (.r‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀)) = ((𝐿 ↑ 𝑀) · ((𝐻‘𝐿) ∗ 1 )))
Theorem	chcoeffeqlem 20509*	Lemma for chcoeffeq 20510. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (𝐶‘𝑀)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 )))
Theorem	chcoeffeq 20510*	The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 8-Dec-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (𝐶‘𝑀)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ))
Theorem	cayhamlem3 20511*	Lemma for cayhamlem4 20512. (Contributed by AV, 24-Nov-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (𝐶‘𝑀)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    &   ⊢ · = (.r‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))))
Theorem	cayhamlem4 20512*	Lemma for cayleyhamilton 20514. (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (𝐶‘𝑀)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑌))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
Theorem	cayleyhamilton0 20513*	The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 20514 provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT 20515)! (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (coe1‘(𝐶‘𝑀))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝑍 = (0g‘𝑌)    &   ⊢ 𝑊 = (Base‘𝑌)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑌))    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, (𝑍 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 𝑍, ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
Theorem	cayleyhamilton 20514*	The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", see theorem 7.8 in [Roman] p. 170 (without proof!), or theorem 3.1 in [Lang] p. 561. In other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. This is Metamath 100 proof #49. (Contributed by Alexander van der Vekens, 25-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (coe1‘(𝐶‘𝑀))    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
Theorem	cayleyhamiltonALT 20515*	Alternate proof of cayleyhamilton 20514, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 20513 directly, but has the same structure as the proof of cayleyhamilton0 20513. In contrast to the proof of cayleyhamilton0 20513, only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (coe1‘(𝐶‘𝑀))    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
Theorem	cayleyhamilton1 20516*	The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton 20514, the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients (𝐹‘𝑛), then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 25-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐾 = (coe1‘(𝐶‘𝑀))    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐴))    &   ⊢ 𝐿 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑍 = (0g‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑𝑚 ℕ0) ∧ 𝐹 finSupp 𝑍)) → ((𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
PART 12  BASIC TOPOLOGY
12.1  Topology
12.1.1  Topological spaces
Syntax	ctop 20517	Extend class notation with the class of all topologies.
class Top
Syntax	ctopon 20518	The class function of all topologies over a base set.
class TopOn
Syntax	ctps 20519	Extend class notation with the class of all topological spaces.
class TopSp
Syntax	ctb 20520	Extend class notation with the class of all topological bases.
class TopBases
Definition	df-top 20521*	Define the (proper) class of all topologies. See istop2g 20526 for an alternate way to express finite intersection. The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.)
⊢ Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)}
Definition	df-bases 20522*	Define the class of all topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 20563). Note that "bases" is the plural of "basis." (Contributed by NM, 17-Jul-2006.)
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
Definition	df-topon 20523*	Define the set of topologies with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})
Definition	df-topsp 20524	Define the class of all topological spaces (structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
Theorem	istopg 20525*	Express the predicate "𝐽 is a topology." Note: In the literature, a topology is often represented by a script letter T, which resembles the letter J. This confusion may have led to J being used by some authors - e.g. K. D. Joshi, Introduction to General Topology (1983), p. 114 - and it is convenient for us since we later use 𝑇 to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
Theorem	istop2g 20526*	Express the predicate "𝐽 is a topology," using "the intersection of the elements of any finite subcollection" instead of the intersection of any two elements. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐽))))
Theorem	uniopn 20527	The union of a subset of a topology is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽)
Theorem	iunopn 20528*	The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.)
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)
Theorem	inopn 20529	The intersection of two open sets of a topology is also an open set. (Contributed by NM, 17-Jul-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)
Theorem	fitop 20530	A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.)
⊢ (𝐽 ∈ Top → (fi‘𝐽) = 𝐽)
Theorem	fiinopn 20531	The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.)
⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴 ∈ 𝐽))
Theorem	iinopn 20532*	The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)
Theorem	unopn 20533	The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∪ 𝐵) ∈ 𝐽)
Theorem	0opn 20534	The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.)
⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)
Theorem	0ntop 20535	The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
⊢ ¬ ∅ ∈ Top
Theorem	topopn 20536	The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
Theorem	eltopss 20537	A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
Theorem	riinopn 20538*	A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ 𝐽)
Theorem	rintopn 20539	A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ∧ 𝐴 ∈ Fin) → (𝑋 ∩ ∩ 𝐴) ∈ 𝐽)
Theorem	istopon 20540	Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
Theorem	topontop 20541	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
Theorem	toponuni 20542	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
Theorem	toponmax 20543	The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)
Theorem	toponss 20544	A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
Theorem	toponcom 20545	If 𝐾 is a topology on the base set of topology 𝐽, then 𝐽 is a topology on the base of 𝐾. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ (TopOn‘∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐾))
Theorem	topontopi 20546	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	toponunii 20547	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐵 = ∪ 𝐽
Theorem	toptopon 20548	Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
Theorem	topgele 20549	The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋))
Theorem	topsn 20550	The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4366). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘{𝐴}) → 𝐽 = 𝒫 {𝐴})
Theorem	istps 20551	Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))
Theorem	istps2 20552	Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽))
Theorem	tpsuni 20553	The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽)
Theorem	tpstop 20554	The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top)
Theorem	tpspropd 20555	A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp))
Theorem	tpsprop2d 20556	A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp))
Theorem	topontopn 20557	Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))
Theorem	tsettps 20558	If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
Theorem	istpsi 20559	Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = 𝐽    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	eltpsg 20560	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
Theorem	eltpsi 20561	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
12.1.2  TopBases for topologies
Theorem	isbasisg 20562*	Express the predicate "𝐵 is a basis for a topology." (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))))
Theorem	isbasis2g 20563*	Express the predicate "𝐵 is a basis for a topology." (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))
Theorem	isbasis3g 20564*	Express the predicate "𝐵 is a basis for a topology." Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))))
Theorem	basis1 20565	Property of a basis. (Contributed by NM, 16-Jul-2006.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷)))
Theorem	basis2 20566*	Property of a basis. (Contributed by NM, 17-Jul-2006.)
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))
Theorem	fiinbas 20567*	If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases)
Theorem	basdif0 20568	A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ((𝐵 ∖ {∅}) ∈ TopBases ↔ 𝐵 ∈ TopBases)
Theorem	baspartn 20569*	A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases)
Theorem	tgval 20570*	The topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)})
Theorem	tgval2 20571*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 20584) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵; see unitg 20582). (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))})
Theorem	eltg 20572	Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴)))
Theorem	eltg2 20573*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))))
Theorem	eltg2b 20574*	Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltg4i 20575	An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴))
Theorem	eltg3i 20576	The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵))
Theorem	eltg3 20577*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥)))
Theorem	tgval3 20578*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)})
Theorem	tg1 20579	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵)
Theorem	tg2 20580*	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))
Theorem	bastg 20581	A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵))
Theorem	unitg 20582	The topology generated by a basis 𝐵 is a topology on ∪ 𝐵. Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.)
⊢ (𝐵 ∈ 𝑉 → ∪ (topGen‘𝐵) = ∪ 𝐵)
Theorem	tgss 20583	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶))
Theorem	tgcl 20584	Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Theorem	tgclb 20585	The property tgcl 20584 can be reversed: if the topology generated by 𝐵 is actually a topology, then 𝐵 must be a topological basis. This yields an alternative definition of TopBases. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top)
Theorem	tgtopon 20586	A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵))
Theorem	topbas 20587	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases)
Theorem	tgtop 20588	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
Theorem	eltop 20589	Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴)))
Theorem	eltop2 20590*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltop3 20591*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥)))
Theorem	fibas 20592	A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (fi‘𝐴) ∈ TopBases
Theorem	tgdom 20593	A space has no more open sets than subsets of a basis. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ≼ 𝒫 𝐵)
Theorem	tgiun 20594*	The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ (topGen‘𝐵))
Theorem	tgidm 20595	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
Theorem	bastop 20596	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
Theorem	tgtop11 20597	The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾)
Theorem	0top 20598	The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006.)
⊢ (𝐽 ∈ Top → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅}))
Theorem	en1top 20599	{∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1𝑜 ↔ 𝐽 = {∅}))
Theorem	en2top 20600	If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2𝑜 ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)))