# 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 ${⊢}{A}={N}\mathrm{Mat}{R}$
matrcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion matrcl ${⊢}{X}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 matrcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matrcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 n0i ${⊢}{X}\in {B}\to ¬{B}=\varnothing$
4 df-mat ${⊢}\mathrm{Mat}=\left({a}\in \mathrm{Fin},{b}\in \mathrm{V}⟼\left({b}\mathrm{freeLMod}\left({a}×{a}\right)\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{b}\mathrm{maMul}⟨{a},{a},{a}⟩⟩\right)$
5 4 mpondm0 ${⊢}¬\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {N}\mathrm{Mat}{R}=\varnothing$
6 1 5 syl5eq ${⊢}¬\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {A}=\varnothing$
7 6 fveq2d ${⊢}¬\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{A}}={\mathrm{Base}}_{\varnothing }$
8 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
9 7 2 8 3eqtr4g ${⊢}¬\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {B}=\varnothing$
10 3 9 nsyl2 ${⊢}{X}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$