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 eqtrid ⊢ ( ( 𝑅 ∈ 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 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 ∈ 𝑈 )