Metamath Proof Explorer


Theorem evlslem1

Description: Lemma for evlseu , give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015) (Proof shortened by AV, 26-Jul-2019) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem1.p 𝑃 = ( 𝐼 mPoly 𝑅 )
evlslem1.b 𝐵 = ( Base ‘ 𝑃 )
evlslem1.c 𝐶 = ( Base ‘ 𝑆 )
evlslem1.d 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
evlslem1.t 𝑇 = ( mulGrp ‘ 𝑆 )
evlslem1.x = ( .g𝑇 )
evlslem1.m · = ( .r𝑆 )
evlslem1.v 𝑉 = ( 𝐼 mVar 𝑅 )
evlslem1.e 𝐸 = ( 𝑝𝐵 ↦ ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
evlslem1.i ( 𝜑𝐼𝑊 )
evlslem1.r ( 𝜑𝑅 ∈ CRing )
evlslem1.s ( 𝜑𝑆 ∈ CRing )
evlslem1.f ( 𝜑𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
evlslem1.g ( 𝜑𝐺 : 𝐼𝐶 )
evlslem1.a 𝐴 = ( algSc ‘ 𝑃 )
Assertion evlslem1 ( 𝜑 → ( 𝐸 ∈ ( 𝑃 RingHom 𝑆 ) ∧ ( 𝐸𝐴 ) = 𝐹 ∧ ( 𝐸𝑉 ) = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 evlslem1.p 𝑃 = ( 𝐼 mPoly 𝑅 )
2 evlslem1.b 𝐵 = ( Base ‘ 𝑃 )
3 evlslem1.c 𝐶 = ( Base ‘ 𝑆 )
4 evlslem1.d 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
5 evlslem1.t 𝑇 = ( mulGrp ‘ 𝑆 )
6 evlslem1.x = ( .g𝑇 )
7 evlslem1.m · = ( .r𝑆 )
8 evlslem1.v 𝑉 = ( 𝐼 mVar 𝑅 )
9 evlslem1.e 𝐸 = ( 𝑝𝐵 ↦ ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
10 evlslem1.i ( 𝜑𝐼𝑊 )
11 evlslem1.r ( 𝜑𝑅 ∈ CRing )
12 evlslem1.s ( 𝜑𝑆 ∈ CRing )
13 evlslem1.f ( 𝜑𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
14 evlslem1.g ( 𝜑𝐺 : 𝐼𝐶 )
15 evlslem1.a 𝐴 = ( algSc ‘ 𝑃 )
16 eqid ( 1r𝑃 ) = ( 1r𝑃 )
17 eqid ( 1r𝑆 ) = ( 1r𝑆 )
18 eqid ( .r𝑃 ) = ( .r𝑃 )
19 11 crngringd ( 𝜑𝑅 ∈ Ring )
20 1 10 19 mplringd ( 𝜑𝑃 ∈ Ring )
21 12 crngringd ( 𝜑𝑆 ∈ Ring )
22 2fveq3 ( 𝑥 = ( 1r𝑅 ) → ( 𝐸 ‘ ( 𝐴𝑥 ) ) = ( 𝐸 ‘ ( 𝐴 ‘ ( 1r𝑅 ) ) ) )
23 fveq2 ( 𝑥 = ( 1r𝑅 ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 1r𝑅 ) ) )
24 22 23 eqeq12d ( 𝑥 = ( 1r𝑅 ) → ( ( 𝐸 ‘ ( 𝐴𝑥 ) ) = ( 𝐹𝑥 ) ↔ ( 𝐸 ‘ ( 𝐴 ‘ ( 1r𝑅 ) ) ) = ( 𝐹 ‘ ( 1r𝑅 ) ) ) )
25 eqid ( 0g𝑅 ) = ( 0g𝑅 )
26 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 10 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐼𝑊 )
28 19 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
29 simpr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
30 1 4 25 26 15 27 28 29 mplascl ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐴𝑥 ) = ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g𝑅 ) ) ) )
31 30 fveq2d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐸 ‘ ( 𝐴𝑥 ) ) = ( 𝐸 ‘ ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g𝑅 ) ) ) ) )
32 11 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
33 12 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑆 ∈ CRing )
34 13 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
35 14 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝐺 : 𝐼𝐶 )
36 4 psrbag0 ( 𝐼𝑊 → ( 𝐼 × { 0 } ) ∈ 𝐷 )
37 10 36 syl ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐷 )
38 37 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 × { 0 } ) ∈ 𝐷 )
39 1 2 3 26 4 5 6 7 8 9 27 32 33 34 35 25 38 29 evlslem3 ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐸 ‘ ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g𝑅 ) ) ) ) = ( ( 𝐹𝑥 ) · ( 𝑇 Σg ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) ) ) )
40 0zd ( ( 𝜑𝑥𝐼 ) → 0 ∈ ℤ )
41 fvexd ( ( 𝜑𝑥𝐼 ) → ( 𝐺𝑥 ) ∈ V )
42 fconstmpt ( 𝐼 × { 0 } ) = ( 𝑥𝐼 ↦ 0 )
43 42 a1i ( 𝜑 → ( 𝐼 × { 0 } ) = ( 𝑥𝐼 ↦ 0 ) )
44 14 feqmptd ( 𝜑𝐺 = ( 𝑥𝐼 ↦ ( 𝐺𝑥 ) ) )
45 10 40 41 43 44 offval2 ( 𝜑 → ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) = ( 𝑥𝐼 ↦ ( 0 ( 𝐺𝑥 ) ) ) )
46 14 ffvelcdmda ( ( 𝜑𝑥𝐼 ) → ( 𝐺𝑥 ) ∈ 𝐶 )
47 5 3 mgpbas 𝐶 = ( Base ‘ 𝑇 )
48 5 17 ringidval ( 1r𝑆 ) = ( 0g𝑇 )
49 47 48 6 mulg0 ( ( 𝐺𝑥 ) ∈ 𝐶 → ( 0 ( 𝐺𝑥 ) ) = ( 1r𝑆 ) )
50 46 49 syl ( ( 𝜑𝑥𝐼 ) → ( 0 ( 𝐺𝑥 ) ) = ( 1r𝑆 ) )
51 50 mpteq2dva ( 𝜑 → ( 𝑥𝐼 ↦ ( 0 ( 𝐺𝑥 ) ) ) = ( 𝑥𝐼 ↦ ( 1r𝑆 ) ) )
52 45 51 eqtrd ( 𝜑 → ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) = ( 𝑥𝐼 ↦ ( 1r𝑆 ) ) )
53 52 oveq2d ( 𝜑 → ( 𝑇 Σg ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) ) = ( 𝑇 Σg ( 𝑥𝐼 ↦ ( 1r𝑆 ) ) ) )
54 5 crngmgp ( 𝑆 ∈ CRing → 𝑇 ∈ CMnd )
55 12 54 syl ( 𝜑𝑇 ∈ CMnd )
56 55 cmnmndd ( 𝜑𝑇 ∈ Mnd )
57 48 gsumz ( ( 𝑇 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝑇 Σg ( 𝑥𝐼 ↦ ( 1r𝑆 ) ) ) = ( 1r𝑆 ) )
58 56 10 57 syl2anc ( 𝜑 → ( 𝑇 Σg ( 𝑥𝐼 ↦ ( 1r𝑆 ) ) ) = ( 1r𝑆 ) )
59 53 58 eqtrd ( 𝜑 → ( 𝑇 Σg ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) ) = ( 1r𝑆 ) )
60 59 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑇 Σg ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) ) = ( 1r𝑆 ) )
61 60 oveq2d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹𝑥 ) · ( 𝑇 Σg ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) ) ) = ( ( 𝐹𝑥 ) · ( 1r𝑆 ) ) )
62 26 3 rhmf ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
63 13 62 syl ( 𝜑𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
64 63 ffvelcdmda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹𝑥 ) ∈ 𝐶 )
65 3 7 17 ringridm ( ( 𝑆 ∈ Ring ∧ ( 𝐹𝑥 ) ∈ 𝐶 ) → ( ( 𝐹𝑥 ) · ( 1r𝑆 ) ) = ( 𝐹𝑥 ) )
66 21 64 65 syl2an2r ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹𝑥 ) · ( 1r𝑆 ) ) = ( 𝐹𝑥 ) )
67 61 66 eqtrd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹𝑥 ) · ( 𝑇 Σg ( ( 𝐼 × { 0 } ) ∘f 𝐺 ) ) ) = ( 𝐹𝑥 ) )
68 31 39 67 3eqtrd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐸 ‘ ( 𝐴𝑥 ) ) = ( 𝐹𝑥 ) )
69 68 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝐸 ‘ ( 𝐴𝑥 ) ) = ( 𝐹𝑥 ) )
70 eqid ( 1r𝑅 ) = ( 1r𝑅 )
71 26 70 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
72 19 71 syl ( 𝜑 → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
73 24 69 72 rspcdva ( 𝜑 → ( 𝐸 ‘ ( 𝐴 ‘ ( 1r𝑅 ) ) ) = ( 𝐹 ‘ ( 1r𝑅 ) ) )
74 1 mplassa ( ( 𝐼𝑊𝑅 ∈ CRing ) → 𝑃 ∈ AssAlg )
75 10 11 74 syl2anc ( 𝜑𝑃 ∈ AssAlg )
76 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
77 15 76 asclrhm ( 𝑃 ∈ AssAlg → 𝐴 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
78 75 77 syl ( 𝜑𝐴 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
79 1 10 11 mplsca ( 𝜑𝑅 = ( Scalar ‘ 𝑃 ) )
80 79 oveq1d ( 𝜑 → ( 𝑅 RingHom 𝑃 ) = ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
81 78 80 eleqtrrd ( 𝜑𝐴 ∈ ( 𝑅 RingHom 𝑃 ) )
82 70 16 rhm1 ( 𝐴 ∈ ( 𝑅 RingHom 𝑃 ) → ( 𝐴 ‘ ( 1r𝑅 ) ) = ( 1r𝑃 ) )
83 81 82 syl ( 𝜑 → ( 𝐴 ‘ ( 1r𝑅 ) ) = ( 1r𝑃 ) )
84 83 fveq2d ( 𝜑 → ( 𝐸 ‘ ( 𝐴 ‘ ( 1r𝑅 ) ) ) = ( 𝐸 ‘ ( 1r𝑃 ) ) )
85 70 17 rhm1 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r𝑅 ) ) = ( 1r𝑆 ) )
86 13 85 syl ( 𝜑 → ( 𝐹 ‘ ( 1r𝑅 ) ) = ( 1r𝑆 ) )
87 73 84 86 3eqtr3d ( 𝜑 → ( 𝐸 ‘ ( 1r𝑃 ) ) = ( 1r𝑆 ) )
88 eqid ( +g𝑃 ) = ( +g𝑃 )
89 eqid ( +g𝑆 ) = ( +g𝑆 )
90 20 ringgrpd ( 𝜑𝑃 ∈ Grp )
91 21 ringgrpd ( 𝜑𝑆 ∈ Grp )
92 eqid ( 0g𝑆 ) = ( 0g𝑆 )
93 ringcmn ( 𝑆 ∈ Ring → 𝑆 ∈ CMnd )
94 21 93 syl ( 𝜑𝑆 ∈ CMnd )
95 94 adantr ( ( 𝜑𝑝𝐵 ) → 𝑆 ∈ CMnd )
96 ovex ( ℕ0m 𝐼 ) ∈ V
97 4 96 rabex2 𝐷 ∈ V
98 97 a1i ( ( 𝜑𝑝𝐵 ) → 𝐷 ∈ V )
99 10 adantr ( ( 𝜑𝑝𝐵 ) → 𝐼𝑊 )
100 11 adantr ( ( 𝜑𝑝𝐵 ) → 𝑅 ∈ CRing )
101 12 adantr ( ( 𝜑𝑝𝐵 ) → 𝑆 ∈ CRing )
102 13 adantr ( ( 𝜑𝑝𝐵 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
103 14 adantr ( ( 𝜑𝑝𝐵 ) → 𝐺 : 𝐼𝐶 )
104 simpr ( ( 𝜑𝑝𝐵 ) → 𝑝𝐵 )
105 1 2 3 4 5 6 7 8 9 99 100 101 102 103 104 evlslem6 ( ( 𝜑𝑝𝐵 ) → ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) : 𝐷𝐶 ∧ ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) finSupp ( 0g𝑆 ) ) )
106 105 simpld ( ( 𝜑𝑝𝐵 ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) : 𝐷𝐶 )
107 105 simprd ( ( 𝜑𝑝𝐵 ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) finSupp ( 0g𝑆 ) )
108 3 92 95 98 106 107 gsumcl ( ( 𝜑𝑝𝐵 ) → ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ∈ 𝐶 )
109 108 9 fmptd ( 𝜑𝐸 : 𝐵𝐶 )
110 eqid ( +g𝑅 ) = ( +g𝑅 )
111 simplrl ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑥𝐵 )
112 simplrr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑦𝐵 )
113 1 2 110 88 111 112 mpladd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝑥 ( +g𝑃 ) 𝑦 ) = ( 𝑥f ( +g𝑅 ) 𝑦 ) )
114 113 fveq1d ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) = ( ( 𝑥f ( +g𝑅 ) 𝑦 ) ‘ 𝑏 ) )
115 simprl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑥𝐵 )
116 1 26 2 4 115 mplelf ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑥 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
117 116 ffnd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑥 Fn 𝐷 )
118 117 adantr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑥 Fn 𝐷 )
119 simprr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑦𝐵 )
120 1 26 2 4 119 mplelf ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑦 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
121 120 ffnd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑦 Fn 𝐷 )
122 121 adantr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑦 Fn 𝐷 )
123 97 a1i ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝐷 ∈ V )
124 simpr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑏𝐷 )
125 fnfvof ( ( ( 𝑥 Fn 𝐷𝑦 Fn 𝐷 ) ∧ ( 𝐷 ∈ V ∧ 𝑏𝐷 ) ) → ( ( 𝑥f ( +g𝑅 ) 𝑦 ) ‘ 𝑏 ) = ( ( 𝑥𝑏 ) ( +g𝑅 ) ( 𝑦𝑏 ) ) )
126 118 122 123 124 125 syl22anc ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝑥f ( +g𝑅 ) 𝑦 ) ‘ 𝑏 ) = ( ( 𝑥𝑏 ) ( +g𝑅 ) ( 𝑦𝑏 ) ) )
127 114 126 eqtrd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) = ( ( 𝑥𝑏 ) ( +g𝑅 ) ( 𝑦𝑏 ) ) )
128 127 fveq2d ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) = ( 𝐹 ‘ ( ( 𝑥𝑏 ) ( +g𝑅 ) ( 𝑦𝑏 ) ) ) )
129 rhmghm ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
130 13 129 syl ( 𝜑𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
131 130 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
132 116 ffvelcdmda ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝑥𝑏 ) ∈ ( Base ‘ 𝑅 ) )
133 120 ffvelcdmda ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝑦𝑏 ) ∈ ( Base ‘ 𝑅 ) )
134 26 110 89 ghmlin ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( 𝑥𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦𝑏 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑥𝑏 ) ( +g𝑅 ) ( 𝑦𝑏 ) ) ) = ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ( +g𝑆 ) ( 𝐹 ‘ ( 𝑦𝑏 ) ) ) )
135 131 132 133 134 syl3anc ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ ( ( 𝑥𝑏 ) ( +g𝑅 ) ( 𝑦𝑏 ) ) ) = ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ( +g𝑆 ) ( 𝐹 ‘ ( 𝑦𝑏 ) ) ) )
136 128 135 eqtrd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ( +g𝑆 ) ( 𝐹 ‘ ( 𝑦𝑏 ) ) ) )
137 136 oveq1d ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ( +g𝑆 ) ( 𝐹 ‘ ( 𝑦𝑏 ) ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) )
138 21 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑆 ∈ Ring )
139 63 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
140 139 132 ffvelcdmd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ ( 𝑥𝑏 ) ) ∈ 𝐶 )
141 139 133 ffvelcdmd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ ( 𝑦𝑏 ) ) ∈ 𝐶 )
142 55 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝑇 ∈ CMnd )
143 14 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → 𝐺 : 𝐼𝐶 )
144 4 47 6 142 124 143 psrbagev2 ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ∈ 𝐶 )
145 3 89 7 ringdir ( ( 𝑆 ∈ Ring ∧ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ∈ 𝐶 ∧ ( 𝐹 ‘ ( 𝑦𝑏 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ∈ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ( +g𝑆 ) ( 𝐹 ‘ ( 𝑦𝑏 ) ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ( +g𝑆 ) ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
146 138 140 141 144 145 syl13anc ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) ( +g𝑆 ) ( 𝐹 ‘ ( 𝑦𝑏 ) ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ( +g𝑆 ) ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
147 137 146 eqtrd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ( +g𝑆 ) ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
148 147 mpteq2dva ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ( +g𝑆 ) ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
149 97 a1i ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐷 ∈ V )
150 ovexd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ∈ V )
151 ovexd ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑏𝐷 ) → ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ∈ V )
152 eqidd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
153 eqidd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
154 149 150 151 152 153 offval2 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ∘f ( +g𝑆 ) ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) = ( 𝑏𝐷 ↦ ( ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ( +g𝑆 ) ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
155 148 154 eqtr4d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ∘f ( +g𝑆 ) ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
156 155 oveq2d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ∘f ( +g𝑆 ) ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ) )
157 94 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑆 ∈ CMnd )
158 10 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐼𝑊 )
159 11 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑅 ∈ CRing )
160 12 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑆 ∈ CRing )
161 13 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
162 14 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐺 : 𝐼𝐶 )
163 1 2 3 4 5 6 7 8 9 158 159 160 161 162 115 evlslem6 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) : 𝐷𝐶 ∧ ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) finSupp ( 0g𝑆 ) ) )
164 163 simpld ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) : 𝐷𝐶 )
165 1 2 3 4 5 6 7 8 9 158 159 160 161 162 119 evlslem6 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) : 𝐷𝐶 ∧ ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) finSupp ( 0g𝑆 ) ) )
166 165 simpld ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) : 𝐷𝐶 )
167 163 simprd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) finSupp ( 0g𝑆 ) )
168 165 simprd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) finSupp ( 0g𝑆 ) )
169 3 92 89 157 149 164 166 167 168 gsumadd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑆 Σg ( ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ∘f ( +g𝑆 ) ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ) = ( ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ( +g𝑆 ) ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ) )
170 156 169 eqtrd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) = ( ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ( +g𝑆 ) ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ) )
171 90 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑃 ∈ Grp )
172 2 88 grpcl ( ( 𝑃 ∈ Grp ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 ( +g𝑃 ) 𝑦 ) ∈ 𝐵 )
173 171 115 119 172 syl3anc ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑃 ) 𝑦 ) ∈ 𝐵 )
174 fveq1 ( 𝑝 = ( 𝑥 ( +g𝑃 ) 𝑦 ) → ( 𝑝𝑏 ) = ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) )
175 174 fveq2d ( 𝑝 = ( 𝑥 ( +g𝑃 ) 𝑦 ) → ( 𝐹 ‘ ( 𝑝𝑏 ) ) = ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) )
176 175 oveq1d ( 𝑝 = ( 𝑥 ( +g𝑃 ) 𝑦 ) → ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) )
177 176 mpteq2dv ( 𝑝 = ( 𝑥 ( +g𝑃 ) 𝑦 ) → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
178 177 oveq2d ( 𝑝 = ( 𝑥 ( +g𝑃 ) 𝑦 ) → ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
179 ovex ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ∈ V
180 178 9 179 fvmpt ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ∈ 𝐵 → ( 𝐸 ‘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
181 173 180 syl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐸 ‘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ( +g𝑃 ) 𝑦 ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
182 fveq1 ( 𝑝 = 𝑥 → ( 𝑝𝑏 ) = ( 𝑥𝑏 ) )
183 182 fveq2d ( 𝑝 = 𝑥 → ( 𝐹 ‘ ( 𝑝𝑏 ) ) = ( 𝐹 ‘ ( 𝑥𝑏 ) ) )
184 183 oveq1d ( 𝑝 = 𝑥 → ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) )
185 184 mpteq2dv ( 𝑝 = 𝑥 → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
186 185 oveq2d ( 𝑝 = 𝑥 → ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
187 ovex ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ∈ V
188 186 9 187 fvmpt ( 𝑥𝐵 → ( 𝐸𝑥 ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
189 115 188 syl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐸𝑥 ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
190 fveq1 ( 𝑝 = 𝑦 → ( 𝑝𝑏 ) = ( 𝑦𝑏 ) )
191 190 fveq2d ( 𝑝 = 𝑦 → ( 𝐹 ‘ ( 𝑝𝑏 ) ) = ( 𝐹 ‘ ( 𝑦𝑏 ) ) )
192 191 oveq1d ( 𝑝 = 𝑦 → ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) = ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) )
193 192 mpteq2dv ( 𝑝 = 𝑦 → ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) )
194 193 oveq2d ( 𝑝 = 𝑦 → ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
195 ovex ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ∈ V
196 194 9 195 fvmpt ( 𝑦𝐵 → ( 𝐸𝑦 ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
197 196 ad2antll ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐸𝑦 ) = ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) )
198 189 197 oveq12d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝐸𝑥 ) ( +g𝑆 ) ( 𝐸𝑦 ) ) = ( ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑥𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ( +g𝑆 ) ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑦𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ) )
199 170 181 198 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐸 ‘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) = ( ( 𝐸𝑥 ) ( +g𝑆 ) ( 𝐸𝑦 ) ) )
200 2 3 88 89 90 91 109 199 isghmd ( 𝜑𝐸 ∈ ( 𝑃 GrpHom 𝑆 ) )
201 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
202 201 5 rhmmhm ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom 𝑇 ) )
203 13 202 syl ( 𝜑𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom 𝑇 ) )
204 203 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom 𝑇 ) )
205 simprll ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑥𝐵 )
206 1 26 2 4 205 mplelf ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑥 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
207 simprrl ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑧𝐷 )
208 206 207 ffvelcdmd ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝑥𝑧 ) ∈ ( Base ‘ 𝑅 ) )
209 simprlr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑦𝐵 )
210 1 26 2 4 209 mplelf ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑦 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
211 simprrr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑤𝐷 )
212 210 211 ffvelcdmd ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝑦𝑤 ) ∈ ( Base ‘ 𝑅 ) )
213 201 26 mgpbas ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
214 eqid ( .r𝑅 ) = ( .r𝑅 )
215 201 214 mgpplusg ( .r𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
216 5 7 mgpplusg · = ( +g𝑇 )
217 213 215 216 mhmlin ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom 𝑇 ) ∧ ( 𝑥𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦𝑤 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ) = ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝐹 ‘ ( 𝑦𝑤 ) ) ) )
218 204 208 212 217 syl3anc ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐹 ‘ ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ) = ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝐹 ‘ ( 𝑦𝑤 ) ) ) )
219 56 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → 𝑇 ∈ Mnd )
220 simprl ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑧𝐷 )
221 4 psrbagf ( 𝑧𝐷𝑧 : 𝐼 ⟶ ℕ0 )
222 220 221 syl ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑧 : 𝐼 ⟶ ℕ0 )
223 222 ffvelcdmda ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝑧𝑣 ) ∈ ℕ0 )
224 4 psrbagf ( 𝑤𝐷𝑤 : 𝐼 ⟶ ℕ0 )
225 224 ad2antll ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑤 : 𝐼 ⟶ ℕ0 )
226 225 ffvelcdmda ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝑤𝑣 ) ∈ ℕ0 )
227 14 adantr ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝐺 : 𝐼𝐶 )
228 227 ffvelcdmda ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝐺𝑣 ) ∈ 𝐶 )
229 47 6 216 mulgnn0dir ( ( 𝑇 ∈ Mnd ∧ ( ( 𝑧𝑣 ) ∈ ℕ0 ∧ ( 𝑤𝑣 ) ∈ ℕ0 ∧ ( 𝐺𝑣 ) ∈ 𝐶 ) ) → ( ( ( 𝑧𝑣 ) + ( 𝑤𝑣 ) ) ( 𝐺𝑣 ) ) = ( ( ( 𝑧𝑣 ) ( 𝐺𝑣 ) ) · ( ( 𝑤𝑣 ) ( 𝐺𝑣 ) ) ) )
230 219 223 226 228 229 syl13anc ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( ( ( 𝑧𝑣 ) + ( 𝑤𝑣 ) ) ( 𝐺𝑣 ) ) = ( ( ( 𝑧𝑣 ) ( 𝐺𝑣 ) ) · ( ( 𝑤𝑣 ) ( 𝐺𝑣 ) ) ) )
231 230 mpteq2dva ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑣𝐼 ↦ ( ( ( 𝑧𝑣 ) + ( 𝑤𝑣 ) ) ( 𝐺𝑣 ) ) ) = ( 𝑣𝐼 ↦ ( ( ( 𝑧𝑣 ) ( 𝐺𝑣 ) ) · ( ( 𝑤𝑣 ) ( 𝐺𝑣 ) ) ) ) )
232 10 adantr ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝐼𝑊 )
233 ovexd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( ( 𝑧𝑣 ) + ( 𝑤𝑣 ) ) ∈ V )
234 fvexd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝐺𝑣 ) ∈ V )
235 222 ffnd ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑧 Fn 𝐼 )
236 225 ffnd ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑤 Fn 𝐼 )
237 inidm ( 𝐼𝐼 ) = 𝐼
238 eqidd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝑧𝑣 ) = ( 𝑧𝑣 ) )
239 eqidd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝑤𝑣 ) = ( 𝑤𝑣 ) )
240 235 236 232 232 237 238 239 offval ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑧f + 𝑤 ) = ( 𝑣𝐼 ↦ ( ( 𝑧𝑣 ) + ( 𝑤𝑣 ) ) ) )
241 14 feqmptd ( 𝜑𝐺 = ( 𝑣𝐼 ↦ ( 𝐺𝑣 ) ) )
242 241 adantr ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝐺 = ( 𝑣𝐼 ↦ ( 𝐺𝑣 ) ) )
243 232 233 234 240 242 offval2 ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) = ( 𝑣𝐼 ↦ ( ( ( 𝑧𝑣 ) + ( 𝑤𝑣 ) ) ( 𝐺𝑣 ) ) ) )
244 ovexd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( ( 𝑧𝑣 ) ( 𝐺𝑣 ) ) ∈ V )
245 ovexd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( ( 𝑤𝑣 ) ( 𝐺𝑣 ) ) ∈ V )
246 14 ffnd ( 𝜑𝐺 Fn 𝐼 )
247 246 adantr ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝐺 Fn 𝐼 )
248 eqidd ( ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) ∧ 𝑣𝐼 ) → ( 𝐺𝑣 ) = ( 𝐺𝑣 ) )
249 235 247 232 232 237 238 248 offval ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑧f 𝐺 ) = ( 𝑣𝐼 ↦ ( ( 𝑧𝑣 ) ( 𝐺𝑣 ) ) ) )
250 236 247 232 232 237 239 248 offval ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑤f 𝐺 ) = ( 𝑣𝐼 ↦ ( ( 𝑤𝑣 ) ( 𝐺𝑣 ) ) ) )
251 232 244 245 249 250 offval2 ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( ( 𝑧f 𝐺 ) ∘f · ( 𝑤f 𝐺 ) ) = ( 𝑣𝐼 ↦ ( ( ( 𝑧𝑣 ) ( 𝐺𝑣 ) ) · ( ( 𝑤𝑣 ) ( 𝐺𝑣 ) ) ) ) )
252 231 243 251 3eqtr4d ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) = ( ( 𝑧f 𝐺 ) ∘f · ( 𝑤f 𝐺 ) ) )
253 252 oveq2d ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑇 Σg ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) ) = ( 𝑇 Σg ( ( 𝑧f 𝐺 ) ∘f · ( 𝑤f 𝐺 ) ) ) )
254 55 adantr ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑇 ∈ CMnd )
255 4 47 6 48 254 220 227 psrbagev1 ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( ( 𝑧f 𝐺 ) : 𝐼𝐶 ∧ ( 𝑧f 𝐺 ) finSupp ( 1r𝑆 ) ) )
256 255 simpld ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑧f 𝐺 ) : 𝐼𝐶 )
257 simprr ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → 𝑤𝐷 )
258 4 47 6 48 254 257 227 psrbagev1 ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( ( 𝑤f 𝐺 ) : 𝐼𝐶 ∧ ( 𝑤f 𝐺 ) finSupp ( 1r𝑆 ) ) )
259 258 simpld ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑤f 𝐺 ) : 𝐼𝐶 )
260 255 simprd ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑧f 𝐺 ) finSupp ( 1r𝑆 ) )
261 258 simprd ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑤f 𝐺 ) finSupp ( 1r𝑆 ) )
262 47 48 216 254 232 256 259 260 261 gsumadd ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑇 Σg ( ( 𝑧f 𝐺 ) ∘f · ( 𝑤f 𝐺 ) ) ) = ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) )
263 253 262 eqtrd ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑇 Σg ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) ) = ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) )
264 263 adantrl ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝑇 Σg ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) ) = ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) )
265 218 264 oveq12d ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ) · ( 𝑇 Σg ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝐹 ‘ ( 𝑦𝑤 ) ) ) · ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) )
266 55 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑇 ∈ CMnd )
267 63 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
268 267 208 ffvelcdmd ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐹 ‘ ( 𝑥𝑧 ) ) ∈ 𝐶 )
269 267 212 ffvelcdmd ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐹 ‘ ( 𝑦𝑤 ) ) ∈ 𝐶 )
270 4 47 6 254 220 227 psrbagev2 ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ∈ 𝐶 )
271 270 adantrl ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ∈ 𝐶 )
272 4 47 6 254 257 227 psrbagev2 ( ( 𝜑 ∧ ( 𝑧𝐷𝑤𝐷 ) ) → ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ∈ 𝐶 )
273 272 adantrl ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ∈ 𝐶 )
274 47 216 cmn4 ( ( 𝑇 ∈ CMnd ∧ ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) ∈ 𝐶 ∧ ( 𝐹 ‘ ( 𝑦𝑤 ) ) ∈ 𝐶 ) ∧ ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ∈ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝐹 ‘ ( 𝑦𝑤 ) ) ) · ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ) · ( ( 𝐹 ‘ ( 𝑦𝑤 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) )
275 266 268 269 271 273 274 syl122anc ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝐹 ‘ ( 𝑦𝑤 ) ) ) · ( ( 𝑇 Σg ( 𝑧f 𝐺 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ) · ( ( 𝐹 ‘ ( 𝑦𝑤 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) )
276 265 275 eqtrd ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ) · ( 𝑇 Σg ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ) · ( ( 𝐹 ‘ ( 𝑦𝑤 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) )
277 10 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝐼𝑊 )
278 11 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑅 ∈ CRing )
279 12 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑆 ∈ CRing )
280 13 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
281 14 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝐺 : 𝐼𝐶 )
282 4 psrbagaddcl ( ( 𝑧𝐷𝑤𝐷 ) → ( 𝑧f + 𝑤 ) ∈ 𝐷 )
283 282 ad2antll ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝑧f + 𝑤 ) ∈ 𝐷 )
284 19 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → 𝑅 ∈ Ring )
285 26 214 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑥𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦𝑤 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ∈ ( Base ‘ 𝑅 ) )
286 284 208 212 285 syl3anc ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ∈ ( Base ‘ 𝑅 ) )
287 1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 283 286 evlslem3 ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = ( 𝑧f + 𝑤 ) , ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) , ( 0g𝑅 ) ) ) ) = ( ( 𝐹 ‘ ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) ) · ( 𝑇 Σg ( ( 𝑧f + 𝑤 ) ∘f 𝐺 ) ) ) )
288 1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 207 208 evlslem3 ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = 𝑧 , ( 𝑥𝑧 ) , ( 0g𝑅 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ) )
289 1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 211 212 evlslem3 ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = 𝑤 , ( 𝑦𝑤 ) , ( 0g𝑅 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑦𝑤 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) )
290 288 289 oveq12d ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = 𝑧 , ( 𝑥𝑧 ) , ( 0g𝑅 ) ) ) ) · ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = 𝑤 , ( 𝑦𝑤 ) , ( 0g𝑅 ) ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑥𝑧 ) ) · ( 𝑇 Σg ( 𝑧f 𝐺 ) ) ) · ( ( 𝐹 ‘ ( 𝑦𝑤 ) ) · ( 𝑇 Σg ( 𝑤f 𝐺 ) ) ) ) )
291 276 287 290 3eqtr4d ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑧𝐷𝑤𝐷 ) ) ) → ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = ( 𝑧f + 𝑤 ) , ( ( 𝑥𝑧 ) ( .r𝑅 ) ( 𝑦𝑤 ) ) , ( 0g𝑅 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = 𝑧 , ( 𝑥𝑧 ) , ( 0g𝑅 ) ) ) ) · ( 𝐸 ‘ ( 𝑣𝐷 ↦ if ( 𝑣 = 𝑤 , ( 𝑦𝑤 ) , ( 0g𝑅 ) ) ) ) ) )
292 1 2 7 25 4 10 11 12 200 291 evlslem2 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐸 ‘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) = ( ( 𝐸𝑥 ) · ( 𝐸𝑦 ) ) )
293 2 16 17 18 7 20 21 87 292 3 88 89 109 199 isrhmd ( 𝜑𝐸 ∈ ( 𝑃 RingHom 𝑆 ) )
294 ovex ( 𝑆 Σg ( 𝑏𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝𝑏 ) ) · ( 𝑇 Σg ( 𝑏f 𝐺 ) ) ) ) ) ∈ V
295 294 9 fnmpti 𝐸 Fn 𝐵
296 295 a1i ( 𝜑𝐸 Fn 𝐵 )
297 26 2 rhmf ( 𝐴 ∈ ( 𝑅 RingHom 𝑃 ) → 𝐴 : ( Base ‘ 𝑅 ) ⟶ 𝐵 )
298 81 297 syl ( 𝜑𝐴 : ( Base ‘ 𝑅 ) ⟶ 𝐵 )
299 298 ffnd ( 𝜑𝐴 Fn ( Base ‘ 𝑅 ) )
300 298 frnd ( 𝜑 → ran 𝐴𝐵 )
301 fnco ( ( 𝐸 Fn 𝐵𝐴 Fn ( Base ‘ 𝑅 ) ∧ ran 𝐴𝐵 ) → ( 𝐸𝐴 ) Fn ( Base ‘ 𝑅 ) )
302 296 299 300 301 syl3anc ( 𝜑 → ( 𝐸𝐴 ) Fn ( Base ‘ 𝑅 ) )
303 63 ffnd ( 𝜑𝐹 Fn ( Base ‘ 𝑅 ) )
304 fvco2 ( ( 𝐴 Fn ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐸𝐴 ) ‘ 𝑥 ) = ( 𝐸 ‘ ( 𝐴𝑥 ) ) )
305 299 304 sylan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐸𝐴 ) ‘ 𝑥 ) = ( 𝐸 ‘ ( 𝐴𝑥 ) ) )
306 305 68 eqtrd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐸𝐴 ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
307 302 303 306 eqfnfvd ( 𝜑 → ( 𝐸𝐴 ) = 𝐹 )
308 1 8 2 10 19 mvrf2 ( 𝜑𝑉 : 𝐼𝐵 )
309 308 ffnd ( 𝜑𝑉 Fn 𝐼 )
310 308 frnd ( 𝜑 → ran 𝑉𝐵 )
311 fnco ( ( 𝐸 Fn 𝐵𝑉 Fn 𝐼 ∧ ran 𝑉𝐵 ) → ( 𝐸𝑉 ) Fn 𝐼 )
312 296 309 310 311 syl3anc ( 𝜑 → ( 𝐸𝑉 ) Fn 𝐼 )
313 fvco2 ( ( 𝑉 Fn 𝐼𝑥𝐼 ) → ( ( 𝐸𝑉 ) ‘ 𝑥 ) = ( 𝐸 ‘ ( 𝑉𝑥 ) ) )
314 309 313 sylan ( ( 𝜑𝑥𝐼 ) → ( ( 𝐸𝑉 ) ‘ 𝑥 ) = ( 𝐸 ‘ ( 𝑉𝑥 ) ) )
315 10 adantr ( ( 𝜑𝑥𝐼 ) → 𝐼𝑊 )
316 11 adantr ( ( 𝜑𝑥𝐼 ) → 𝑅 ∈ CRing )
317 simpr ( ( 𝜑𝑥𝐼 ) → 𝑥𝐼 )
318 8 4 25 70 315 316 317 mvrval ( ( 𝜑𝑥𝐼 ) → ( 𝑉𝑥 ) = ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) )
319 318 fveq2d ( ( 𝜑𝑥𝐼 ) → ( 𝐸 ‘ ( 𝑉𝑥 ) ) = ( 𝐸 ‘ ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) )
320 12 adantr ( ( 𝜑𝑥𝐼 ) → 𝑆 ∈ CRing )
321 13 adantr ( ( 𝜑𝑥𝐼 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
322 14 adantr ( ( 𝜑𝑥𝐼 ) → 𝐺 : 𝐼𝐶 )
323 4 psrbagsn ( 𝐼𝑊 → ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∈ 𝐷 )
324 10 323 syl ( 𝜑 → ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∈ 𝐷 )
325 324 adantr ( ( 𝜑𝑥𝐼 ) → ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∈ 𝐷 )
326 72 adantr ( ( 𝜑𝑥𝐼 ) → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
327 1 2 3 26 4 5 6 7 8 9 315 316 320 321 322 25 325 326 evlslem3 ( ( 𝜑𝑥𝐼 ) → ( 𝐸 ‘ ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) = ( ( 𝐹 ‘ ( 1r𝑅 ) ) · ( 𝑇 Σg ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) ) ) )
328 86 adantr ( ( 𝜑𝑥𝐼 ) → ( 𝐹 ‘ ( 1r𝑅 ) ) = ( 1r𝑆 ) )
329 1nn0 1 ∈ ℕ0
330 0nn0 0 ∈ ℕ0
331 329 330 ifcli if ( 𝑧 = 𝑥 , 1 , 0 ) ∈ ℕ0
332 331 a1i ( ( 𝜑𝑧𝐼 ) → if ( 𝑧 = 𝑥 , 1 , 0 ) ∈ ℕ0 )
333 14 ffvelcdmda ( ( 𝜑𝑧𝐼 ) → ( 𝐺𝑧 ) ∈ 𝐶 )
334 eqidd ( 𝜑 → ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) )
335 14 feqmptd ( 𝜑𝐺 = ( 𝑧𝐼 ↦ ( 𝐺𝑧 ) ) )
336 10 332 333 334 335 offval2 ( 𝜑 → ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) = ( 𝑧𝐼 ↦ ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) ) )
337 oveq1 ( 1 = if ( 𝑧 = 𝑥 , 1 , 0 ) → ( 1 ( 𝐺𝑧 ) ) = ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) )
338 337 eqeq1d ( 1 = if ( 𝑧 = 𝑥 , 1 , 0 ) → ( ( 1 ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ↔ ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) )
339 oveq1 ( 0 = if ( 𝑧 = 𝑥 , 1 , 0 ) → ( 0 ( 𝐺𝑧 ) ) = ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) )
340 339 eqeq1d ( 0 = if ( 𝑧 = 𝑥 , 1 , 0 ) → ( ( 0 ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ↔ ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) )
341 333 adantr ( ( ( 𝜑𝑧𝐼 ) ∧ 𝑧 = 𝑥 ) → ( 𝐺𝑧 ) ∈ 𝐶 )
342 47 6 mulg1 ( ( 𝐺𝑧 ) ∈ 𝐶 → ( 1 ( 𝐺𝑧 ) ) = ( 𝐺𝑧 ) )
343 341 342 syl ( ( ( 𝜑𝑧𝐼 ) ∧ 𝑧 = 𝑥 ) → ( 1 ( 𝐺𝑧 ) ) = ( 𝐺𝑧 ) )
344 iftrue ( 𝑧 = 𝑥 → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 𝐺𝑧 ) )
345 344 adantl ( ( ( 𝜑𝑧𝐼 ) ∧ 𝑧 = 𝑥 ) → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 𝐺𝑧 ) )
346 343 345 eqtr4d ( ( ( 𝜑𝑧𝐼 ) ∧ 𝑧 = 𝑥 ) → ( 1 ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) )
347 47 48 6 mulg0 ( ( 𝐺𝑧 ) ∈ 𝐶 → ( 0 ( 𝐺𝑧 ) ) = ( 1r𝑆 ) )
348 333 347 syl ( ( 𝜑𝑧𝐼 ) → ( 0 ( 𝐺𝑧 ) ) = ( 1r𝑆 ) )
349 348 adantr ( ( ( 𝜑𝑧𝐼 ) ∧ ¬ 𝑧 = 𝑥 ) → ( 0 ( 𝐺𝑧 ) ) = ( 1r𝑆 ) )
350 iffalse ( ¬ 𝑧 = 𝑥 → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 1r𝑆 ) )
351 350 adantl ( ( ( 𝜑𝑧𝐼 ) ∧ ¬ 𝑧 = 𝑥 ) → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 1r𝑆 ) )
352 349 351 eqtr4d ( ( ( 𝜑𝑧𝐼 ) ∧ ¬ 𝑧 = 𝑥 ) → ( 0 ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) )
353 338 340 346 352 ifbothda ( ( 𝜑𝑧𝐼 ) → ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) = if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) )
354 353 mpteq2dva ( 𝜑 → ( 𝑧𝐼 ↦ ( if ( 𝑧 = 𝑥 , 1 , 0 ) ( 𝐺𝑧 ) ) ) = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) )
355 336 354 eqtrd ( 𝜑 → ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) )
356 355 adantr ( ( 𝜑𝑥𝐼 ) → ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) )
357 356 oveq2d ( ( 𝜑𝑥𝐼 ) → ( 𝑇 Σg ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) ) = ( 𝑇 Σg ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) ) )
358 56 adantr ( ( 𝜑𝑥𝐼 ) → 𝑇 ∈ Mnd )
359 333 adantlr ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑧𝐼 ) → ( 𝐺𝑧 ) ∈ 𝐶 )
360 3 17 ringidcl ( 𝑆 ∈ Ring → ( 1r𝑆 ) ∈ 𝐶 )
361 21 360 syl ( 𝜑 → ( 1r𝑆 ) ∈ 𝐶 )
362 361 ad2antrr ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑧𝐼 ) → ( 1r𝑆 ) ∈ 𝐶 )
363 359 362 ifcld ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑧𝐼 ) → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ∈ 𝐶 )
364 363 fmpttd ( ( 𝜑𝑥𝐼 ) → ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) : 𝐼𝐶 )
365 eldifsnneq ( 𝑧 ∈ ( 𝐼 ∖ { 𝑥 } ) → ¬ 𝑧 = 𝑥 )
366 365 350 syl ( 𝑧 ∈ ( 𝐼 ∖ { 𝑥 } ) → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 1r𝑆 ) )
367 366 adantl ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑧 ∈ ( 𝐼 ∖ { 𝑥 } ) ) → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 1r𝑆 ) )
368 367 315 suppss2 ( ( 𝜑𝑥𝐼 ) → ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) supp ( 1r𝑆 ) ) ⊆ { 𝑥 } )
369 47 48 358 315 317 364 368 gsumpt ( ( 𝜑𝑥𝐼 ) → ( 𝑇 Σg ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) ) = ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) ‘ 𝑥 ) )
370 fveq2 ( 𝑧 = 𝑥 → ( 𝐺𝑧 ) = ( 𝐺𝑥 ) )
371 344 370 eqtrd ( 𝑧 = 𝑥 → if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) = ( 𝐺𝑥 ) )
372 eqid ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) = ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) )
373 fvex ( 𝐺𝑥 ) ∈ V
374 371 372 373 fvmpt ( 𝑥𝐼 → ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
375 374 adantl ( ( 𝜑𝑥𝐼 ) → ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , ( 𝐺𝑧 ) , ( 1r𝑆 ) ) ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
376 357 369 375 3eqtrd ( ( 𝜑𝑥𝐼 ) → ( 𝑇 Σg ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) ) = ( 𝐺𝑥 ) )
377 328 376 oveq12d ( ( 𝜑𝑥𝐼 ) → ( ( 𝐹 ‘ ( 1r𝑅 ) ) · ( 𝑇 Σg ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) ) ) = ( ( 1r𝑆 ) · ( 𝐺𝑥 ) ) )
378 3 7 17 ringlidm ( ( 𝑆 ∈ Ring ∧ ( 𝐺𝑥 ) ∈ 𝐶 ) → ( ( 1r𝑆 ) · ( 𝐺𝑥 ) ) = ( 𝐺𝑥 ) )
379 21 46 378 syl2an2r ( ( 𝜑𝑥𝐼 ) → ( ( 1r𝑆 ) · ( 𝐺𝑥 ) ) = ( 𝐺𝑥 ) )
380 377 379 eqtrd ( ( 𝜑𝑥𝐼 ) → ( ( 𝐹 ‘ ( 1r𝑅 ) ) · ( 𝑇 Σg ( ( 𝑧𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∘f 𝐺 ) ) ) = ( 𝐺𝑥 ) )
381 319 327 380 3eqtrd ( ( 𝜑𝑥𝐼 ) → ( 𝐸 ‘ ( 𝑉𝑥 ) ) = ( 𝐺𝑥 ) )
382 314 381 eqtrd ( ( 𝜑𝑥𝐼 ) → ( ( 𝐸𝑉 ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
383 312 246 382 eqfnfvd ( 𝜑 → ( 𝐸𝑉 ) = 𝐺 )
384 293 307 383 3jca ( 𝜑 → ( 𝐸 ∈ ( 𝑃 RingHom 𝑆 ) ∧ ( 𝐸𝐴 ) = 𝐹 ∧ ( 𝐸𝑉 ) = 𝐺 ) )