This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )