Theorem mat0dimid

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

	Ref	Expression
Hypothesis	mat0dim.a	⊢ 𝐴 = ( ∅ Mat 𝑅 )
Assertion	mat0dimid	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝐴 ) = ∅ )

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		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
6		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
7	5 6	ringidcl	⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
8	4 7	syl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
9	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
10		mat0dimbas0	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
11	9 10	eqtrid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝐴 ) = { ∅ } )
12	11	eleq2d	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ↔ ( 1r ‘ 𝐴 ) ∈ { ∅ } ) )
13		elsni	⊢ ( ( 1r ‘ 𝐴 ) ∈ { ∅ } → ( 1r ‘ 𝐴 ) = ∅ )
14	12 13	biimtrdi	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) → ( 1r ‘ 𝐴 ) = ∅ ) )
15	8 14	mpd	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝐴 ) = ∅ )