Metamath Proof Explorer

Theorem prdslmodd

Description: The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdslmodd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdslmodd.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
prdslmodd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
prdslmodd.rm ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
prdslmodd.rs ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
Assertion prdslmodd ( 𝜑 → 𝑌 ∈ LMod )

Proof

Step Hyp Ref Expression
1 prdslmodd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdslmodd.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
3 prdslmodd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 prdslmodd.rm ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
5 prdslmodd.rs ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
6 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
7 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) )
8 4 3 fexd ⊢ ( 𝜑 → 𝑅 ∈ V )
9 1 2 8 prdssca ⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑌 ) )
10 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 ) )
11 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
12 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) )
13 eqidd ⊢ ( 𝜑 → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) )
14 eqidd ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 ) )
15 lmodgrp ⊢ ( 𝑎 ∈ LMod → 𝑎 ∈ Grp )
16 15 ssriv ⊢ LMod ⊆ Grp
17 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ LMod ∧ LMod ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp )
18 4 16 17 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
19 1 3 2 18 prdsgrpd ⊢ ( 𝜑 → 𝑌 ∈ Grp )
20 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
21 eqid ⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
22 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
23 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
24 3 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
26 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ LMod )
27 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
29 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
30 1 20 21 22 23 25 26 27 28 29 prdsvscacl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
31 30 3impb ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
32 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
33 32 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
34 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
35 5 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ 𝑆 ) )
36 35 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ 𝑆 ) )
37 34 36 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
38 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ Ring )
39 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
40 4 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
41 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
42 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
43 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
44 1 20 38 39 41 42 43 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
45 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
46 1 20 38 39 41 45 43 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
47 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
48 eqid ⊢ ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑦 ) )
49 eqid ⊢ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) )
50 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) )
51 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
52 47 48 49 50 51 lmodvsdi ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
53 33 37 44 46 52 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
54 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
55 1 20 38 39 41 42 45 54 43 prdsplusgfval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
56 55 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
57 1 20 21 22 38 39 41 34 42 43 prdsvscafval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) )
58 1 20 21 22 38 39 41 34 45 43 prdsvscafval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
59 57 58 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
60 53 56 59 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
61 60 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
62 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
63 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
64 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 Fn 𝐼 )
65 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
66 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑌 ∈ Grp )
67 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
68 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
69 20 54 grpcl ⊢ ( ( 𝑌 ∈ Grp ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
70 66 67 68 69 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
71 1 20 21 22 62 63 64 65 70 prdsvscaval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
72 30 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
73 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
74 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
75 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ LMod )
76 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
77 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
78 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
79 1 20 21 22 73 74 75 76 77 78 prdsvscacl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
80 79 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
81 1 20 62 63 64 72 80 54 prdsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
82 61 71 81 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) )
83 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ Ring )
84 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
85 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
86 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
87 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
88 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
89 1 20 21 22 83 84 85 86 87 88 prdsvscafval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
90 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
91 1 20 21 22 83 84 85 90 87 88 prdsvscafval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
92 89 91 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
93 32 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
94 35 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ 𝑆 ) )
95 86 94 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
96 90 94 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
97 1 20 83 84 85 87 88 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
98 eqid ⊢ ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
99 47 48 49 50 51 98 lmodvsdir ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
100 93 95 96 97 99 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
101 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
102 101 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( +g ‘ 𝑆 ) )
103 102 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) )
104 103 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
105 92 100 104 3eqtr2rd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
106 105 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
107 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
108 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
109 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 Fn 𝐼 )
110 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
111 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
112 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
113 22 112 ringacl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
114 107 110 111 113 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
115 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
116 1 20 21 22 107 108 109 114 115 prdsvscaval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
117 79 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
118 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ LMod )
119 1 20 21 22 107 108 118 111 115 101 prdsvscacl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
120 1 20 107 108 109 117 119 54 prdsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
121 106 116 120 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) )
122 91 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
123 eqid ⊢ ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
124 47 49 50 51 123 lmodvsass ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
125 93 95 96 97 124 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
126 101 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( .r ‘ 𝑆 ) )
127 126 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) )
128 127 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
129 122 125 128 3eqtr2rd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
130 129 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
131 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
132 22 131 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
133 107 110 111 132 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
134 1 20 21 22 107 108 109 133 115 prdsvscaval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
135 1 20 21 22 107 108 109 110 119 prdsvscaval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
136 130 134 135 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) )
137 5 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 1r ‘ 𝑆 ) )
138 137 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 1r ‘ 𝑆 ) )
139 138 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) )
140 32 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
141 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ Ring )
142 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
143 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
144 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
145 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
146 1 20 141 142 143 144 145 prdsbasprj ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
147 eqid ⊢ ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
148 47 49 50 147 lmodvs1 ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) → ( ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( 𝑎 ‘ 𝑦 ) )
149 140 146 148 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( 𝑎 ‘ 𝑦 ) )
150 139 149 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( 𝑎 ‘ 𝑦 ) )
151 150 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑦 ) ) )
152 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑆 ∈ Ring )
153 24 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝐼 ∈ V )
154 40 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 Fn 𝐼 )
155 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
156 22 155 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
157 2 156 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
158 157 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
159 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
160 1 20 21 22 152 153 154 158 159 prdsvscaval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ 𝑌 ) 𝑎 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) ) )
161 1 20 152 153 154 159 prdsbasfn ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 Fn 𝐼 )
162 dffn5 ⊢ ( 𝑎 Fn 𝐼 ↔ 𝑎 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑦 ) ) )
163 161 162 sylib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑦 ) ) )
164 151 160 163 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ 𝑌 ) 𝑎 ) = 𝑎 )
165 6 7 9 10 11 12 13 14 2 19 31 82 121 136 164 islmodd ⊢ ( 𝜑 → 𝑌 ∈ LMod )