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 ‘ 𝑅 ) ⟩ } )