Metamath Proof Explorer


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 syl5eq ( ¬ ( 𝑁 ∈ 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 ) )