Theorem mat0dim0

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

	Ref	Expression
Hypothesis	mat0dim.a	⊢ 𝐴 = ( ∅ Mat 𝑅 )
Assertion	mat0dim0	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mat0dim.a	⊢ 𝐴 = ( ∅ Mat 𝑅 )
2		0fi	⊢ ∅ ∈ Fin
3	1	matring	⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
4	2 3	mpan	⊢ ( 𝑅 ∈ Ring → 𝐴 ∈ Ring )
5		ringgrp	⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ Grp )
6		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
7		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
8	6 7	grpidcl	⊢ ( 𝐴 ∈ Grp → ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
9	4 5 8	3syl	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
10	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
11		mat0dimbas0	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
12	10 11	eqtrid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝐴 ) = { ∅ } )
13	12	eleq2d	⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ↔ ( 0g ‘ 𝐴 ) ∈ { ∅ } ) )
14		elsni	⊢ ( ( 0g ‘ 𝐴 ) ∈ { ∅ } → ( 0g ‘ 𝐴 ) = ∅ )
15	13 14	biimtrdi	⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) → ( 0g ‘ 𝐴 ) = ∅ ) )
16	9 15	mpd	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝐴 ) = ∅ )