Step |
Hyp |
Ref |
Expression |
1 |
|
rmsuppfi.r |
|- R = ( Base ` M ) |
2 |
|
simp3 |
|- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( A supp ( 0g ` M ) ) e. Fin ) |
3 |
1
|
rmsuppss |
|- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) ) |
4 |
3
|
3adant3 |
|- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) ) |
5 |
|
ssfi |
|- ( ( ( A supp ( 0g ` M ) ) e. Fin /\ ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin ) |
6 |
2 4 5
|
syl2anc |
|- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin ) |