This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ⊢ ( ℕ0 ↑m 𝐼 ) ∈ 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 𝑆 ) ∧ ( 𝐸 ∘ 𝐴 ) = 𝐹 ∧ ( 𝐸 ∘ 𝑉 ) = 𝐺 ) )