This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat1dim0

Description: The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019)

Ref Expression
Hypotheses mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion mat1dim0 ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 0g ‘ 𝐴 ) = { ⟨ 𝑂 , ( 0g ‘ 𝑅 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4 snfi ⊢ { 𝐸 } ∈ Fin
5 4 a1i ⊢ ( 𝐸 ∈ 𝑉 → { 𝐸 } ∈ Fin )
6 5 anim2i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑅 ∈ Ring ∧ { 𝐸 } ∈ Fin ) )
7 6 ancomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 1 8 mat0op ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) ) )
10 7 9 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) ) )
11 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ 𝑉 )
12 fvexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 0g ‘ 𝑅 ) ∈ V )
13 eqid ⊢ ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) )
14 eqidd ⊢ ( 𝑥 = 𝐸 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
15 eqidd ⊢ ( 𝑦 = 𝐸 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
16 13 14 15 mposn ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ ( 0g ‘ 𝑅 ) ∈ V ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 0g ‘ 𝑅 ) ⟩ } )
17 3 eqcomi ⊢ ⟨ 𝐸 , 𝐸 ⟩ = 𝑂
18 17 opeq1i ⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 0g ‘ 𝑅 ) ⟩ = ⟨ 𝑂 , ( 0g ‘ 𝑅 ) ⟩
19 18 sneqi ⊢ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 0g ‘ 𝑅 ) ⟩ } = { ⟨ 𝑂 , ( 0g ‘ 𝑅 ) ⟩ }
20 16 19 eqtrdi ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ ( 0g ‘ 𝑅 ) ∈ V ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) ) = { ⟨ 𝑂 , ( 0g ‘ 𝑅 ) ⟩ } )
21 11 11 12 20 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ ( 0g ‘ 𝑅 ) ) = { ⟨ 𝑂 , ( 0g ‘ 𝑅 ) ⟩ } )
22 10 21 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 0g ‘ 𝐴 ) = { ⟨ 𝑂 , ( 0g ‘ 𝑅 ) ⟩ } )