Metamath Proof Explorer

Theorem frlmlss

Description: The base set of the free module is a subspace of the power module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses frlmval.f 
|- F = ( R freeLMod I )
frlmpws.b 
|- B = ( Base ` F )
frlmlss.u 
|- U = ( LSubSp ` ( ( ringLMod ` R ) ^s I ) )
Assertion frlmlss 
|- ( ( R e. Ring /\ I e. W ) -> B e. U )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 frlmpws.b 
 |-  B = ( Base ` F )
3 frlmlss.u 
 |-  U = ( LSubSp ` ( ( ringLMod ` R ) ^s I ) )
4 1 frlmval 
 |-  ( ( R e. Ring /\ I e. W ) -> F = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )
5 4 fveq2d 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` F ) = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
6 2 5 syl5eq 
 |-  ( ( R e. Ring /\ I e. W ) -> B = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
7 simpr 
 |-  ( ( R e. Ring /\ I e. W ) -> I e. W )
8 simpl 
 |-  ( ( R e. Ring /\ I e. W ) -> R e. Ring )
9 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
10 9 adantr 
 |-  ( ( R e. Ring /\ I e. W ) -> ( ringLMod ` R ) e. LMod )
11 fconst6g 
 |-  ( ( ringLMod ` R ) e. LMod -> ( I X. { ( ringLMod ` R ) } ) : I --> LMod )
12 10 11 syl 
 |-  ( ( R e. Ring /\ I e. W ) -> ( I X. { ( ringLMod ` R ) } ) : I --> LMod )
13 fvex 
 |-  ( ringLMod ` R ) e. _V
14 13 fvconst2 
 |-  ( i e. I -> ( ( I X. { ( ringLMod ` R ) } ) ` i ) = ( ringLMod ` R ) )
15 14 adantl 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( ( I X. { ( ringLMod ` R ) } ) ` i ) = ( ringLMod ` R ) )
16 15 fveq2d 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( Scalar ` ( ( I X. { ( ringLMod ` R ) } ) ` i ) ) = ( Scalar ` ( ringLMod ` R ) ) )
17 rlmsca 
 |-  ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) )
18 17 ad2antrr 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
19 16 18 eqtr4d 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( Scalar ` ( ( I X. { ( ringLMod ` R ) } ) ` i ) ) = R )
20 eqid 
 |-  ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) )
21 eqid 
 |-  ( LSubSp ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) = ( LSubSp ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
22 eqid 
 |-  ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )
23 7 8 12 19 20 21 22 dsmmlss 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) e. ( LSubSp ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) )
24 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
25 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
26 24 25 pwsval 
 |-  ( ( ( ringLMod ` R ) e. _V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
27 13 26 mpan 
 |-  ( I e. W -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
28 27 adantl 
 |-  ( ( R e. Ring /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
29 17 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` ( ringLMod ` R ) ) = R )
30 29 adantr 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Scalar ` ( ringLMod ` R ) ) = R )
31 30 oveq1d 
 |-  ( ( R e. Ring /\ I e. W ) -> ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
32 28 31 eqtr2d 
 |-  ( ( R e. Ring /\ I e. W ) -> ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( ( ringLMod ` R ) ^s I ) )
33 32 fveq2d 
 |-  ( ( R e. Ring /\ I e. W ) -> ( LSubSp ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) = ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) )
34 33 3 eqtr4di 
 |-  ( ( R e. Ring /\ I e. W ) -> ( LSubSp ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) = U )
35 23 34 eleqtrd 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) e. U )
36 6 35 eqeltrd 
 |-  ( ( R e. Ring /\ I e. W ) -> B e. U )