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 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmpws.b 𝐵 = ( Base ‘ 𝐹 )
frlmlss.u 𝑈 = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
Assertion frlmlss ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐵𝑈 )

Proof

Step Hyp Ref Expression
1 frlmval.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmpws.b 𝐵 = ( Base ‘ 𝐹 )
3 frlmlss.u 𝑈 = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
4 1 frlmval ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐹 = ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
5 4 fveq2d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) )
6 2 5 syl5eq ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐵 = ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) )
7 simpr ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐼𝑊 )
8 simpl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝑅 ∈ Ring )
9 rlmlmod ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
10 9 adantr ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
11 fconst6g ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) : 𝐼 ⟶ LMod )
12 10 11 syl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) : 𝐼 ⟶ LMod )
13 fvex ( ringLMod ‘ 𝑅 ) ∈ V
14 13 fvconst2 ( 𝑖𝐼 → ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) = ( ringLMod ‘ 𝑅 ) )
15 14 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) = ( ringLMod ‘ 𝑅 ) )
16 15 fveq2d ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → ( Scalar ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
17 rlmsca ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
18 17 ad2antrr ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
19 16 18 eqtr4d ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → ( Scalar ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) ) = 𝑅 )
20 eqid ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) )
21 eqid ( LSubSp ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( LSubSp ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
22 eqid ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
23 7 8 12 19 20 21 22 dsmmlss ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ ( LSubSp ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) )
24 eqid ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
25 eqid ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
26 24 25 pwsval ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
27 13 26 mpan ( 𝐼𝑊 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
28 27 adantl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
29 17 eqcomd ( 𝑅 ∈ Ring → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = 𝑅 )
30 29 adantr ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = 𝑅 )
31 30 oveq1d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
32 28 31 eqtr2d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
33 32 fveq2d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( LSubSp ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
34 33 3 eqtr4di ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( LSubSp ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = 𝑈 )
35 23 34 eleqtrd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ 𝑈 )
36 6 35 eqeltrd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐵𝑈 )