mat0dim0

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

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

Step	Hyp	Ref	Expression
1		mat0dim.a	$⊢ A = \emptyset Mat R$
2		0fi	$⊢ \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		ringgrp	$⊢ A \in Ring \to A \in Grp$
6		eqid	$⊢ {Base}_{A} = {Base}_{A}$
7		eqid	$⊢ 0_{A} = 0_{A}$
8	6 7	grpidcl	$⊢ A \in Grp \to 0_{A} \in {Base}_{A}$
9	4 5 8	3syl	$⊢ R \in Ring \to 0_{A} \in {Base}_{A}$
10	1	fveq2i	$⊢ {Base}_{A} = {Base}_{(\emptyset Mat R)}$
11		mat0dimbas0	$⊢ R \in Ring \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
12	10 11	eqtrid	$⊢ R \in Ring \to {Base}_{A} = \{\emptyset\}$
13	12	eleq2d	$⊢ R \in Ring \to (0_{A} \in {Base}_{A} \leftrightarrow 0_{A} \in \{\emptyset\})$
14		elsni	$⊢ 0_{A} \in \{\emptyset\} \to 0_{A} = \emptyset$
15	13 14	biimtrdi	$⊢ R \in Ring \to (0_{A} \in {Base}_{A} \to 0_{A} = \emptyset)$
16	9 15	mpd	$⊢ R \in Ring \to 0_{A} = \emptyset$

Metamath Proof Explorer