Theorem matrcl

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

	Ref	Expression
Hypotheses	matrcl.a	|- A = ( N Mat R )
	matrcl.b	|- B = ( Base ` A )
Assertion	matrcl	|- ( X e. B -> ( N e. Fin /\ R e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		matrcl.a	|- A = ( N Mat R )
2		matrcl.b	|- B = ( Base ` A )
3		n0i	|- ( X e. B -> -. B = (/) )
4		df-mat	|- Mat = ( a e. Fin , b e. _V |-> ( ( b freeLMod ( a X. a ) ) sSet <. ( .r ` ndx ) , ( b maMul <. a , a , a >. ) >. ) )
5	4	mpondm0	|- ( -. ( N e. Fin /\ R e. _V ) -> ( N Mat R ) = (/) )
6	1 5	eqtrid	|- ( -. ( N e. Fin /\ R e. _V ) -> A = (/) )
7	6	fveq2d	|- ( -. ( N e. Fin /\ R e. _V ) -> ( Base ` A ) = ( Base ` (/) ) )
8		base0	|- (/) = ( Base ` (/) )
9	7 2 8	3eqtr4g	|- ( -. ( N e. Fin /\ R e. _V ) -> B = (/) )
10	3 9	nsyl2	|- ( X e. B -> ( N e. Fin /\ R e. _V ) )