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