Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  matrcl Structured version   Visualization version   GIF version

Theorem matrcl 21097
 Description: Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Hypotheses
Ref Expression
matrcl.a 𝐴 = (𝑁 Mat 𝑅)
matrcl.b 𝐵 = (Base‘𝐴)
Assertion
Ref Expression
matrcl (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))

Proof of Theorem matrcl
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4228 . 2 (𝑋𝐵 → ¬ 𝐵 = ∅)
2 matrcl.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
3 df-mat 21093 . . . . . 6 Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
43mpondm0 7375 . . . . 5 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
52, 4syl5eq 2806 . . . 4 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
65fveq2d 6655 . . 3 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7 matrcl.b . . 3 𝐵 = (Base‘𝐴)
8 base0 16579 . . 3 ∅ = (Base‘∅)
96, 7, 83eqtr4g 2819 . 2 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
101, 9nsyl2 143 1 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))