Metamath Proof Explorer

Theorem prdsvscacl

Description: Pointwise scalar multiplication is closed in products of modules. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsvscacl.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsvscacl.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsvscacl.t ⊢ · = ( ·𝑠 ‘ 𝑌 )
prdsvscacl.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
prdsvscacl.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
prdsvscacl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsvscacl.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
prdsvscacl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
prdsvscacl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
prdsvscacl.sr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = 𝑆 )
Assertion prdsvscacl ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 prdsvscacl.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsvscacl.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsvscacl.t ⊢ · = ( ·𝑠 ‘ 𝑌 )
4 prdsvscacl.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
5 prdsvscacl.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
6 prdsvscacl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7 prdsvscacl.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
8 prdsvscacl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
9 prdsvscacl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10 prdsvscacl.sr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = 𝑆 )
11 7 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
12 1 2 3 4 5 6 11 8 9 prdsvscaval ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
13 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ LMod )
14 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐹 ∈ 𝐾 )
15 10 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ 𝑆 ) )
16 15 4 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = 𝐾 )
17 14 16 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐹 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
18 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ Ring )
19 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
20 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
21 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ 𝐵 )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
23 1 2 18 19 20 21 22 prdsbasprj ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
24 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
25 eqid ⊢ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) )
26 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) )
27 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) )
28 24 25 26 27 lmodvscl ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ LMod ∧ 𝐹 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
29 13 17 23 28 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
31 1 2 5 6 11 prdsbasmpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
32 30 31 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ 𝐵 )
33 12 32 eqeltrd ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )