mat0dimid

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

		Ref	Expression
	Hypothesis	mat0dim.a	$⊢ A = \emptyset Mat R$
	Assertion	mat0dimid	$⊢ R \in Ring \to 1_{A} = \emptyset$

Step	Hyp	Ref	Expression
1		mat0dim.a	$⊢ A = \emptyset Mat R$
2		0fin	$⊢ \emptyset \in Fin$
3	1	matring	$⊢ (\emptyset \in Fin \land R \in Ring) \to A \in Ring$
4	2 3	mpan	$⊢ R \in Ring \to A \in Ring$
5		eqid	$⊢ {Base}_{A} = {Base}_{A}$
6		eqid	$⊢ 1_{A} = 1_{A}$
7	5 6	ringidcl	$⊢ A \in Ring \to 1_{A} \in {Base}_{A}$
8	4 7	syl	$⊢ R \in Ring \to 1_{A} \in {Base}_{A}$
9	1	fveq2i	$⊢ {Base}_{A} = {Base}_{(\emptyset Mat R)}$
10		mat0dimbas0	$⊢ R \in Ring \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
11	9 10	eqtrid	$⊢ R \in Ring \to {Base}_{A} = \{\emptyset\}$
12	11	eleq2d	$⊢ R \in Ring \to (1_{A} \in {Base}_{A} \leftrightarrow 1_{A} \in \{\emptyset\})$
13		elsni	$⊢ 1_{A} \in \{\emptyset\} \to 1_{A} = \emptyset$
14	12 13	syl6bi	$⊢ R \in Ring \to (1_{A} \in {Base}_{A} \to 1_{A} = \emptyset)$
15	8 14	mpd	$⊢ R \in Ring \to 1_{A} = \emptyset$

Metamath Proof Explorer