Theorem matrcl

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

	Ref	Expression
Hypotheses	matrcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matrcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		matrcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matrcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		n0i	⊢ ( 𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅ )
4		df-mat	⊢ Mat = ( 𝑎 ∈ Fin , 𝑏 ∈ V ↦ ( ( 𝑏 freeLMod ( 𝑎 × 𝑎 ) ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑏 maMul ⟨ 𝑎 , 𝑎 , 𝑎 ⟩ ) ⟩ ) )
5	4	mpondm0	⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ∅ )
6	1 5	eqtrid	⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝐴 = ∅ )
7	6	fveq2d	⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ 𝐴 ) = ( Base ‘ ∅ ) )
8		base0	⊢ ∅ = ( Base ‘ ∅ )
9	7 2 8	3eqtr4g	⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
10	3 9	nsyl2	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )