Theorem matrcl

Description: Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	matrcl.a	$$⊢A=N\mathrm{Mat}R$$
	matrcl.b	$$⊢B={\mathrm{Base}}_A$$
Assertion	matrcl	$$⊢X\in B\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		matrcl.a	$$⊢A=N\mathrm{Mat}R$$
2		matrcl.b	$$⊢B={\mathrm{Base}}_A$$
3		n0i	$$⊢X\in B\to \neg B=\varnothing$$
4		df-mat	$$⊢\mathrm{Mat}=\left(a\in \mathrm{Fin},b\in \mathrm{V}⟼\left(b\mathrm{freeLMod}\left(a\times a\right)\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},b\mathrm{maMul}⟨a,a,a⟩⟩\right)$$
5	4	mpondm0	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to N\mathrm{Mat}R=\varnothing$$
6	1 5	syl5eq	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to A=\varnothing$$
7	6	fveq2d	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_A={\mathrm{Base}}_{\varnothing }$$
8		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
9	7 2 8	3eqtr4g	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to B=\varnothing$$
10	3 9	nsyl2	$$⊢X\in B\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)$$