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