Description: Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | matrcl.a | |- A = ( N Mat R ) |
|
matrcl.b | |- B = ( Base ` A ) |
||
Assertion | matrcl | |- ( X e. B -> ( N e. Fin /\ R e. _V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | matrcl.a | |- A = ( N Mat R ) |
|
2 | matrcl.b | |- B = ( Base ` A ) |
|
3 | n0i | |- ( X e. B -> -. B = (/) ) |
|
4 | df-mat | |- Mat = ( a e. Fin , b e. _V |-> ( ( b freeLMod ( a X. a ) ) sSet <. ( .r ` ndx ) , ( b maMul <. a , a , a >. ) >. ) ) |
|
5 | 4 | mpondm0 | |- ( -. ( N e. Fin /\ R e. _V ) -> ( N Mat R ) = (/) ) |
6 | 1 5 | syl5eq | |- ( -. ( N e. Fin /\ R e. _V ) -> A = (/) ) |
7 | 6 | fveq2d | |- ( -. ( N e. Fin /\ R e. _V ) -> ( Base ` A ) = ( Base ` (/) ) ) |
8 | base0 | |- (/) = ( Base ` (/) ) |
|
9 | 7 2 8 | 3eqtr4g | |- ( -. ( N e. Fin /\ R e. _V ) -> B = (/) ) |
10 | 3 9 | nsyl2 | |- ( X e. B -> ( N e. Fin /\ R e. _V ) ) |