Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  evlslem1 Structured version   Visualization version   GIF version

Theorem evlslem1 20757
 Description: Lemma for evlseu 20758, 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.)
Hypotheses
Ref Expression
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
Ref Expression
evlslem1 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸𝐴) = 𝐹 ∧ (𝐸𝑉) = 𝐺))
Distinct variable groups:   𝑝,𝑏,𝐵   𝐶,𝑏,𝑝   𝜑,𝑏,𝑝   𝐹,𝑏,𝑝   𝑇,𝑏,𝑝   𝐷,𝑏,𝑝   ,𝑏,𝐼,𝑝   𝑅,𝑏,,𝑝   𝐺,𝑏,𝑝   𝑃,𝑏,𝑝   𝑆,𝑏,𝑝   · ,𝑏,𝑝   ,𝑏,𝑝
Allowed substitution hints:   𝜑()   𝐴(,𝑝,𝑏)   𝐵()   𝐶()   𝐷()   𝑃()   𝑆()   𝑇()   · ()   𝐸(,𝑝,𝑏)   ()   𝐹()   𝐺()   𝑉(,𝑝,𝑏)   𝑊(,𝑝,𝑏)

Proof of Theorem evlslem1
Dummy variables 𝑥 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evlslem1.b . . 3 𝐵 = (Base‘𝑃)
2 eqid 2801 . . 3 (1r𝑃) = (1r𝑃)
3 eqid 2801 . . 3 (1r𝑆) = (1r𝑆)
4 eqid 2801 . . 3 (.r𝑃) = (.r𝑃)
5 evlslem1.m . . 3 · = (.r𝑆)
6 evlslem1.i . . . 4 (𝜑𝐼𝑊)
7 evlslem1.r . . . . 5 (𝜑𝑅 ∈ CRing)
8 crngring 19305 . . . . 5 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
97, 8syl 17 . . . 4 (𝜑𝑅 ∈ Ring)
10 evlslem1.p . . . . 5 𝑃 = (𝐼 mPoly 𝑅)
1110mplring 20694 . . . 4 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ Ring)
126, 9, 11syl2anc 587 . . 3 (𝜑𝑃 ∈ Ring)
13 evlslem1.s . . . 4 (𝜑𝑆 ∈ CRing)
14 crngring 19305 . . . 4 (𝑆 ∈ CRing → 𝑆 ∈ Ring)
1513, 14syl 17 . . 3 (𝜑𝑆 ∈ Ring)
16 2fveq3 6654 . . . . . 6 (𝑥 = (1r𝑅) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝐴‘(1r𝑅))))
17 fveq2 6649 . . . . . 6 (𝑥 = (1r𝑅) → (𝐹𝑥) = (𝐹‘(1r𝑅)))
1816, 17eqeq12d 2817 . . . . 5 (𝑥 = (1r𝑅) → ((𝐸‘(𝐴𝑥)) = (𝐹𝑥) ↔ (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅))))
19 evlslem1.d . . . . . . . . 9 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
20 eqid 2801 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
21 eqid 2801 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
22 evlslem1.a . . . . . . . . 9 𝐴 = (algSc‘𝑃)
236adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐼𝑊)
249adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
25 simpr 488 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
2610, 19, 20, 21, 22, 23, 24, 25mplascl 20738 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐴𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅))))
2726fveq2d 6653 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))))
28 evlslem1.c . . . . . . . 8 𝐶 = (Base‘𝑆)
29 evlslem1.t . . . . . . . 8 𝑇 = (mulGrp‘𝑆)
30 evlslem1.x . . . . . . . 8 = (.g𝑇)
31 evlslem1.v . . . . . . . 8 𝑉 = (𝐼 mVar 𝑅)
32 evlslem1.e . . . . . . . 8 𝐸 = (𝑝𝐵 ↦ (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
337adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
3413adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing)
35 evlslem1.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
3635adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
37 evlslem1.g . . . . . . . . 9 (𝜑𝐺:𝐼𝐶)
3837adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼𝐶)
3919psrbag0 20736 . . . . . . . . . 10 (𝐼𝑊 → (𝐼 × {0}) ∈ 𝐷)
406, 39syl 17 . . . . . . . . 9 (𝜑 → (𝐼 × {0}) ∈ 𝐷)
4140adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷)
4210, 1, 28, 21, 19, 29, 30, 5, 31, 32, 23, 33, 34, 36, 38, 20, 41, 25evlslem3 20755 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))) = ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))))
43 0zd 11985 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → 0 ∈ ℤ)
44 fvexd 6664 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ V)
45 fconstmpt 5582 . . . . . . . . . . . . . . 15 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
4645a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 × {0}) = (𝑥𝐼 ↦ 0))
4737feqmptd 6712 . . . . . . . . . . . . . 14 (𝜑𝐺 = (𝑥𝐼 ↦ (𝐺𝑥)))
486, 43, 44, 46, 47offval2 7410 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 × {0}) ∘f 𝐺) = (𝑥𝐼 ↦ (0 (𝐺𝑥))))
4937ffvelrnda 6832 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ 𝐶)
5029, 28mgpbas 19241 . . . . . . . . . . . . . . . 16 𝐶 = (Base‘𝑇)
5129, 3ringidval 19249 . . . . . . . . . . . . . . . 16 (1r𝑆) = (0g𝑇)
5250, 51, 30mulg0 18226 . . . . . . . . . . . . . . 15 ((𝐺𝑥) ∈ 𝐶 → (0 (𝐺𝑥)) = (1r𝑆))
5349, 52syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (0 (𝐺𝑥)) = (1r𝑆))
5453mpteq2dva 5128 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐼 ↦ (0 (𝐺𝑥))) = (𝑥𝐼 ↦ (1r𝑆)))
5548, 54eqtrd 2836 . . . . . . . . . . . 12 (𝜑 → ((𝐼 × {0}) ∘f 𝐺) = (𝑥𝐼 ↦ (1r𝑆)))
5655oveq2d 7155 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))))
5729crngmgp 19301 . . . . . . . . . . . . . 14 (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
5813, 57syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ CMnd)
59 cmnmnd 18917 . . . . . . . . . . . . 13 (𝑇 ∈ CMnd → 𝑇 ∈ Mnd)
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑𝑇 ∈ Mnd)
6151gsumz 17995 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝐼𝑊) → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
6260, 6, 61syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
6356, 62eqtrd 2836 . . . . . . . . . 10 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (1r𝑆))
6463adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (1r𝑆))
6564oveq2d 7155 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))) = ((𝐹𝑥) · (1r𝑆)))
6621, 28rhmf 19477 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
6735, 66syl 17 . . . . . . . . . 10 (𝜑𝐹:(Base‘𝑅)⟶𝐶)
6867ffvelrnda 6832 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐹𝑥) ∈ 𝐶)
6928, 5, 3ringridm 19321 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ (𝐹𝑥) ∈ 𝐶) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
7015, 68, 69syl2an2r 684 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
7165, 70eqtrd 2836 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))) = (𝐹𝑥))
7227, 42, 713eqtrd 2840 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
7372ralrimiva 3152 . . . . 5 (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴𝑥)) = (𝐹𝑥))
74 eqid 2801 . . . . . . 7 (1r𝑅) = (1r𝑅)
7521, 74ringidcl 19317 . . . . . 6 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
769, 75syl 17 . . . . 5 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
7718, 73, 76rspcdva 3576 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅)))
7810mplassa 20697 . . . . . . . . 9 ((𝐼𝑊𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
796, 7, 78syl2anc 587 . . . . . . . 8 (𝜑𝑃 ∈ AssAlg)
80 eqid 2801 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
8122, 80asclrhm 20579 . . . . . . . 8 (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
8279, 81syl 17 . . . . . . 7 (𝜑𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
8310, 6, 7mplsca 20687 . . . . . . . 8 (𝜑𝑅 = (Scalar‘𝑃))
8483oveq1d 7154 . . . . . . 7 (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
8582, 84eleqtrrd 2896 . . . . . 6 (𝜑𝐴 ∈ (𝑅 RingHom 𝑃))
8674, 2rhm1 19481 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r𝑅)) = (1r𝑃))
8785, 86syl 17 . . . . 5 (𝜑 → (𝐴‘(1r𝑅)) = (1r𝑃))
8887fveq2d 6653 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐸‘(1r𝑃)))
8974, 3rhm1 19481 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r𝑅)) = (1r𝑆))
9035, 89syl 17 . . . 4 (𝜑 → (𝐹‘(1r𝑅)) = (1r𝑆))
9177, 88, 903eqtr3d 2844 . . 3 (𝜑 → (𝐸‘(1r𝑃)) = (1r𝑆))
92 eqid 2801 . . . . 5 (+g𝑃) = (+g𝑃)
93 eqid 2801 . . . . 5 (+g𝑆) = (+g𝑆)
94 ringgrp 19298 . . . . . 6 (𝑃 ∈ Ring → 𝑃 ∈ Grp)
9512, 94syl 17 . . . . 5 (𝜑𝑃 ∈ Grp)
96 ringgrp 19298 . . . . . 6 (𝑆 ∈ Ring → 𝑆 ∈ Grp)
9715, 96syl 17 . . . . 5 (𝜑𝑆 ∈ Grp)
98 eqid 2801 . . . . . . 7 (0g𝑆) = (0g𝑆)
99 ringcmn 19330 . . . . . . . . 9 (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
10015, 99syl 17 . . . . . . . 8 (𝜑𝑆 ∈ CMnd)
101100adantr 484 . . . . . . 7 ((𝜑𝑝𝐵) → 𝑆 ∈ CMnd)
102 ovex 7172 . . . . . . . . 9 (ℕ0m 𝐼) ∈ V
10319, 102rabex2 5204 . . . . . . . 8 𝐷 ∈ V
104103a1i 11 . . . . . . 7 ((𝜑𝑝𝐵) → 𝐷 ∈ V)
1056adantr 484 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐼𝑊)
1067adantr 484 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑅 ∈ CRing)
10713adantr 484 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑆 ∈ CRing)
10835adantr 484 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
10937adantr 484 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐺:𝐼𝐶)
110 simpr 488 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑝𝐵)
11110, 1, 28, 19, 29, 30, 5, 31, 32, 105, 106, 107, 108, 109, 110evlslem6 20756 . . . . . . . 8 ((𝜑𝑝𝐵) → ((𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
112111simpld 498 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
113111simprd 499 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
11428, 98, 101, 104, 112, 113gsumcl 19031 . . . . . 6 ((𝜑𝑝𝐵) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ 𝐶)
115114, 32fmptd 6859 . . . . 5 (𝜑𝐸:𝐵𝐶)
116 eqid 2801 . . . . . . . . . . . . . . . . 17 (+g𝑅) = (+g𝑅)
117 simplrl 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥𝐵)
118 simplrr 777 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦𝐵)
11910, 1, 116, 92, 117, 118mpladd 20683 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥(+g𝑃)𝑦) = (𝑥f (+g𝑅)𝑦))
120119fveq1d 6651 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥f (+g𝑅)𝑦)‘𝑏))
121 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
12210, 21, 1, 19, 121mplelf 20674 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥:𝐷⟶(Base‘𝑅))
123122ffnd 6492 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 Fn 𝐷)
124123adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥 Fn 𝐷)
125 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
12610, 21, 1, 19, 125mplelf 20674 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦:𝐷⟶(Base‘𝑅))
127126ffnd 6492 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 Fn 𝐷)
128127adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦 Fn 𝐷)
129103a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐷 ∈ V)
130 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑏𝐷)
131 fnfvof 7407 . . . . . . . . . . . . . . . 16 (((𝑥 Fn 𝐷𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏𝐷)) → ((𝑥f (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
132124, 128, 129, 130, 131syl22anc 837 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥f (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
133120, 132eqtrd 2836 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
134133fveq2d 6653 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))))
135 rhmghm 19476 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
13635, 135syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ (𝑅 GrpHom 𝑆))
137136ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
138122ffvelrnda 6832 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥𝑏) ∈ (Base‘𝑅))
139126ffvelrnda 6832 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑦𝑏) ∈ (Base‘𝑅))
14021, 116, 93ghmlin 18358 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥𝑏) ∈ (Base‘𝑅) ∧ (𝑦𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
141137, 138, 139, 140syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
142134, 141eqtrd 2836 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
143142oveq1d 7154 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))))
14415ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑆 ∈ Ring)
14567ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
146145, 138ffvelrnd 6833 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑥𝑏)) ∈ 𝐶)
147145, 139ffvelrnd 6833 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑦𝑏)) ∈ 𝐶)
14858ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑇 ∈ CMnd)
14937ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐺:𝐼𝐶)
1506ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐼𝑊)
15119, 50, 30, 148, 130, 149, 150psrbagev2 20753 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑇 Σg (𝑏f 𝐺)) ∈ 𝐶)
15228, 93, 5ringdir 19316 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏f 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
153144, 146, 147, 151, 152syl13anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
154143, 153eqtrd 2836 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
155154mpteq2dva 5128 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
156103a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐷 ∈ V)
157 ovexd 7174 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))) ∈ V)
158 ovexd 7174 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))) ∈ V)
159 eqidd 2802 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
160 eqidd 2802 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
161156, 157, 158, 159, 160offval2 7410 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
162155, 161eqtr4d 2839 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
163162oveq2d 7155 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
164100adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CMnd)
1656adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐼𝑊)
1667adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ CRing)
16713adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CRing)
16835adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
16937adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺:𝐼𝐶)
17010, 1, 28, 19, 29, 30, 5, 31, 32, 165, 166, 167, 168, 169, 121evlslem6 20756 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
171170simpld 498 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
17210, 1, 28, 19, 29, 30, 5, 31, 32, 165, 166, 167, 168, 169, 125evlslem6 20756 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
173172simpld 498 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
174170simprd 499 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
175172simprd 499 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
17628, 98, 93, 164, 156, 171, 173, 174, 175gsumadd 19039 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
177163, 176eqtrd 2836 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
17895adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Grp)
1791, 92grpcl 18106 . . . . . . . 8 ((𝑃 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
180178, 121, 125, 179syl3anc 1368 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
181 fveq1 6648 . . . . . . . . . . . 12 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑝𝑏) = ((𝑥(+g𝑃)𝑦)‘𝑏))
182181fveq2d 6653 . . . . . . . . . . 11 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝐹‘(𝑝𝑏)) = (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)))
183182oveq1d 7154 . . . . . . . . . 10 (𝑝 = (𝑥(+g𝑃)𝑦) → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
184183mpteq2dv 5129 . . . . . . . . 9 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
185184oveq2d 7155 . . . . . . . 8 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
186 ovex 7172 . . . . . . . 8 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
187185, 32, 186fvmpt 6749 . . . . . . 7 ((𝑥(+g𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
188180, 187syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
189 fveq1 6648 . . . . . . . . . . . . 13 (𝑝 = 𝑥 → (𝑝𝑏) = (𝑥𝑏))
190189fveq2d 6653 . . . . . . . . . . . 12 (𝑝 = 𝑥 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑥𝑏)))
191190oveq1d 7154 . . . . . . . . . . 11 (𝑝 = 𝑥 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
192191mpteq2dv 5129 . . . . . . . . . 10 (𝑝 = 𝑥 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
193192oveq2d 7155 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
194 ovex 7172 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
195193, 32, 194fvmpt 6749 . . . . . . . 8 (𝑥𝐵 → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
196121, 195syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
197 fveq1 6648 . . . . . . . . . . . . 13 (𝑝 = 𝑦 → (𝑝𝑏) = (𝑦𝑏))
198197fveq2d 6653 . . . . . . . . . . . 12 (𝑝 = 𝑦 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑦𝑏)))
199198oveq1d 7154 . . . . . . . . . . 11 (𝑝 = 𝑦 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
200199mpteq2dv 5129 . . . . . . . . . 10 (𝑝 = 𝑦 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
201200oveq2d 7155 . . . . . . . . 9 (𝑝 = 𝑦 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
202 ovex 7172 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
203201, 32, 202fvmpt 6749 . . . . . . . 8 (𝑦𝐵 → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
204203ad2antll 728 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
205196, 204oveq12d 7157 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐸𝑥)(+g𝑆)(𝐸𝑦)) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
206177, 188, 2053eqtr4d 2846 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = ((𝐸𝑥)(+g𝑆)(𝐸𝑦)))
2071, 28, 92, 93, 95, 97, 115, 206isghmd 18362 . . . 4 (𝜑𝐸 ∈ (𝑃 GrpHom 𝑆))
208 eqid 2801 . . . . . . . . . . 11 (mulGrp‘𝑅) = (mulGrp‘𝑅)
209208, 29rhmmhm 19473 . . . . . . . . . 10 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
21035, 209syl 17 . . . . . . . . 9 (𝜑𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
211210adantr 484 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
212 simprll 778 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥𝐵)
21310, 21, 1, 19, 212mplelf 20674 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥:𝐷⟶(Base‘𝑅))
214 simprrl 780 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑧𝐷)
215213, 214ffvelrnd 6833 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑥𝑧) ∈ (Base‘𝑅))
216 simprlr 779 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦𝐵)
21710, 21, 1, 19, 216mplelf 20674 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦:𝐷⟶(Base‘𝑅))
218 simprrr 781 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑤𝐷)
219217, 218ffvelrnd 6833 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑦𝑤) ∈ (Base‘𝑅))
220208, 21mgpbas 19241 . . . . . . . . 9 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
221 eqid 2801 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
222208, 221mgpplusg 19239 . . . . . . . . 9 (.r𝑅) = (+g‘(mulGrp‘𝑅))
22329, 5mgpplusg 19239 . . . . . . . . 9 · = (+g𝑇)
224220, 222, 223mhmlin 17958 . . . . . . . 8 ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥𝑧) ∈ (Base‘𝑅) ∧ (𝑦𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
225211, 215, 219, 224syl3anc 1368 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
22660ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → 𝑇 ∈ Mnd)
227 simprl 770 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧𝐷)
22819psrbagf 20606 . . . . . . . . . . . . . . 15 ((𝐼𝑊𝑧𝐷) → 𝑧:𝐼⟶ℕ0)
2296, 227, 228syl2an2r 684 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧:𝐼⟶ℕ0)
230229ffvelrnda 6832 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) ∈ ℕ0)
231 simprr 772 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤𝐷)
23219psrbagf 20606 . . . . . . . . . . . . . . 15 ((𝐼𝑊𝑤𝐷) → 𝑤:𝐼⟶ℕ0)
2336, 231, 232syl2an2r 684 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤:𝐼⟶ℕ0)
234233ffvelrnda 6832 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) ∈ ℕ0)
23537adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺:𝐼𝐶)
236235ffvelrnda 6832 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ 𝐶)
23750, 30, 223mulgnn0dir 18252 . . . . . . . . . . . . 13 ((𝑇 ∈ Mnd ∧ ((𝑧𝑣) ∈ ℕ0 ∧ (𝑤𝑣) ∈ ℕ0 ∧ (𝐺𝑣) ∈ 𝐶)) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
238226, 230, 234, 236, 237syl13anc 1369 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
239238mpteq2dva 5128 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
2406adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐼𝑊)
241 ovexd 7174 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) + (𝑤𝑣)) ∈ V)
242 fvexd 6664 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ V)
243229ffnd 6492 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧 Fn 𝐼)
244233ffnd 6492 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤 Fn 𝐼)
245 inidm 4148 . . . . . . . . . . . . 13 (𝐼𝐼) = 𝐼
246 eqidd 2802 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) = (𝑧𝑣))
247 eqidd 2802 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) = (𝑤𝑣))
248243, 244, 240, 240, 245, 246, 247offval 7400 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f + 𝑤) = (𝑣𝐼 ↦ ((𝑧𝑣) + (𝑤𝑣))))
24937feqmptd 6712 . . . . . . . . . . . . 13 (𝜑𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
250249adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
251240, 241, 242, 248, 250offval2 7410 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f + 𝑤) ∘f 𝐺) = (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))))
252 ovexd 7174 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) (𝐺𝑣)) ∈ V)
253 ovexd 7174 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑤𝑣) (𝐺𝑣)) ∈ V)
25437ffnd 6492 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐼)
255254adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 Fn 𝐼)
256 eqidd 2802 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) = (𝐺𝑣))
257243, 255, 240, 240, 245, 246, 256offval 7400 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺) = (𝑣𝐼 ↦ ((𝑧𝑣) (𝐺𝑣))))
258244, 255, 240, 240, 245, 247, 256offval 7400 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺) = (𝑣𝐼 ↦ ((𝑤𝑣) (𝐺𝑣))))
259240, 252, 253, 257, 258offval2 7410 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f 𝐺) ∘f · (𝑤f 𝐺)) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
260239, 251, 2593eqtr4d 2846 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f + 𝑤) ∘f 𝐺) = ((𝑧f 𝐺) ∘f · (𝑤f 𝐺)))
261260oveq2d 7155 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = (𝑇 Σg ((𝑧f 𝐺) ∘f · (𝑤f 𝐺))))
26258adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑇 ∈ CMnd)
26319, 50, 30, 51, 262, 227, 235, 240psrbagev1 20752 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f 𝐺):𝐼𝐶 ∧ (𝑧f 𝐺) finSupp (1r𝑆)))
264263simpld 498 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺):𝐼𝐶)
26519, 50, 30, 51, 262, 231, 235, 240psrbagev1 20752 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑤f 𝐺):𝐼𝐶 ∧ (𝑤f 𝐺) finSupp (1r𝑆)))
266265simpld 498 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺):𝐼𝐶)
267263simprd 499 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺) finSupp (1r𝑆))
268265simprd 499 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺) finSupp (1r𝑆))
26950, 51, 223, 262, 240, 264, 266, 267, 268gsumadd 19039 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f 𝐺) ∘f · (𝑤f 𝐺))) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
270261, 269eqtrd 2836 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
271270adantrl 715 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
272225, 271oveq12d 7157 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))))
27358adantr 484 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑇 ∈ CMnd)
27467adantr 484 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶)
275274, 215ffvelrnd 6833 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑥𝑧)) ∈ 𝐶)
276274, 219ffvelrnd 6833 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑦𝑤)) ∈ 𝐶)
27719, 50, 30, 262, 227, 235, 240psrbagev2 20753 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶)
278277adantrl 715 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶)
27919, 50, 30, 262, 231, 235, 240psrbagev2 20753 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)
280279adantrl 715 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)
28150, 223cmn4 18921 . . . . . . 7 ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
282273, 275, 276, 278, 280, 281syl122anc 1376 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
283272, 282eqtrd 2836 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
2846adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐼𝑊)
2857adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ CRing)
28613adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑆 ∈ CRing)
28735adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
28837adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐺:𝐼𝐶)
28919psrbagaddcl 20611 . . . . . . 7 ((𝐼𝑊𝑧𝐷𝑤𝐷) → (𝑧f + 𝑤) ∈ 𝐷)
290284, 214, 218, 289syl3anc 1368 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑧f + 𝑤) ∈ 𝐷)
2919adantr 484 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ Ring)
29221, 221ringcl 19310 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑥𝑧) ∈ (Base‘𝑅) ∧ (𝑦𝑤) ∈ (Base‘𝑅)) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ (Base‘𝑅))
293291, 215, 219, 292syl3anc 1368 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ (Base‘𝑅))
29410, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 290, 293evlslem3 20755 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧f + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))))
29510, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 214, 215evlslem3 20755 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) = ((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))))
29610, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 218, 219evlslem3 20755 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅)))) = ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺))))
297295, 296oveq12d 7157 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
298283, 294, 2973eqtr4d 2846 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧f + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))))
29910, 1, 5, 20, 19, 6, 7, 13, 207, 298evlslem2 20754 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(.r𝑃)𝑦)) = ((𝐸𝑥) · (𝐸𝑦)))
3001, 2, 3, 4, 5, 12, 15, 91, 299, 28, 92, 93, 115, 206isrhmd 19480 . 2 (𝜑𝐸 ∈ (𝑃 RingHom 𝑆))
301 ovex 7172 . . . . . 6 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
302301, 32fnmpti 6467 . . . . 5 𝐸 Fn 𝐵
303302a1i 11 . . . 4 (𝜑𝐸 Fn 𝐵)
30421, 1rhmf 19477 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵)
30585, 304syl 17 . . . . 5 (𝜑𝐴:(Base‘𝑅)⟶𝐵)
306305ffnd 6492 . . . 4 (𝜑𝐴 Fn (Base‘𝑅))
307305frnd 6498 . . . 4 (𝜑 → ran 𝐴𝐵)
308 fnco 6441 . . . 4 ((𝐸 Fn 𝐵𝐴 Fn (Base‘𝑅) ∧ ran 𝐴𝐵) → (𝐸𝐴) Fn (Base‘𝑅))
309303, 306, 307, 308syl3anc 1368 . . 3 (𝜑 → (𝐸𝐴) Fn (Base‘𝑅))
31067ffnd 6492 . . 3 (𝜑𝐹 Fn (Base‘𝑅))
311 fvco2 6739 . . . . 5 ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
312306, 311sylan 583 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
313312, 72eqtrd 2836 . . 3 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐹𝑥))
314309, 310, 313eqfnfvd 6786 . 2 (𝜑 → (𝐸𝐴) = 𝐹)
31510, 31, 1, 6, 9mvrf2 20734 . . . . 5 (𝜑𝑉:𝐼𝐵)
316315ffnd 6492 . . . 4 (𝜑𝑉 Fn 𝐼)
317315frnd 6498 . . . 4 (𝜑 → ran 𝑉𝐵)
318 fnco 6441 . . . 4 ((𝐸 Fn 𝐵𝑉 Fn 𝐼 ∧ ran 𝑉𝐵) → (𝐸𝑉) Fn 𝐼)
319303, 316, 317, 318syl3anc 1368 . . 3 (𝜑 → (𝐸𝑉) Fn 𝐼)
320 fvco2 6739 . . . . 5 ((𝑉 Fn 𝐼𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
321316, 320sylan 583 . . . 4 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
3226adantr 484 . . . . . . 7 ((𝜑𝑥𝐼) → 𝐼𝑊)
3237adantr 484 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑅 ∈ CRing)
324 simpr 488 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑥𝐼)
32531, 19, 20, 74, 322, 323, 324mvrval 20662 . . . . . 6 ((𝜑𝑥𝐼) → (𝑉𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅))))
326325fveq2d 6653 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))))
32713adantr 484 . . . . . 6 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
32835adantr 484 . . . . . 6 ((𝜑𝑥𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
32937adantr 484 . . . . . 6 ((𝜑𝑥𝐼) → 𝐺:𝐼𝐶)
33019psrbagsn 20737 . . . . . . . 8 (𝐼𝑊 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
3316, 330syl 17 . . . . . . 7 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
332331adantr 484 . . . . . 6 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
33376adantr 484 . . . . . 6 ((𝜑𝑥𝐼) → (1r𝑅) ∈ (Base‘𝑅))
33410, 1, 28, 21, 19, 29, 30, 5, 31, 32, 322, 323, 327, 328, 329, 20, 332, 333evlslem3 20755 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))) = ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))))
33590adantr 484 . . . . . . 7 ((𝜑𝑥𝐼) → (𝐹‘(1r𝑅)) = (1r𝑆))
336 1nn0 11905 . . . . . . . . . . . . . 14 1 ∈ ℕ0
337 0nn0 11904 . . . . . . . . . . . . . 14 0 ∈ ℕ0
338336, 337ifcli 4474 . . . . . . . . . . . . 13 if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
339338a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
34037ffvelrnda 6832 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
341 eqidd 2802 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
34237feqmptd 6712 . . . . . . . . . . . 12 (𝜑𝐺 = (𝑧𝐼 ↦ (𝐺𝑧)))
3436, 339, 340, 341, 342offval2 7410 . . . . . . . . . . 11 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))))
344 oveq1 7146 . . . . . . . . . . . . . 14 (1 = if(𝑧 = 𝑥, 1, 0) → (1 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
345344eqeq1d 2803 . . . . . . . . . . . . 13 (1 = if(𝑧 = 𝑥, 1, 0) → ((1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
346 oveq1 7146 . . . . . . . . . . . . . 14 (0 = if(𝑧 = 𝑥, 1, 0) → (0 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
347346eqeq1d 2803 . . . . . . . . . . . . 13 (0 = if(𝑧 = 𝑥, 1, 0) → ((0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
348340adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (𝐺𝑧) ∈ 𝐶)
34950, 30mulg1 18230 . . . . . . . . . . . . . . 15 ((𝐺𝑧) ∈ 𝐶 → (1 (𝐺𝑧)) = (𝐺𝑧))
350348, 349syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = (𝐺𝑧))
351 iftrue 4434 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
352351adantl 485 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
353350, 352eqtr4d 2839 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
35450, 51, 30mulg0 18226 . . . . . . . . . . . . . . . 16 ((𝐺𝑧) ∈ 𝐶 → (0 (𝐺𝑧)) = (1r𝑆))
355340, 354syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐼) → (0 (𝐺𝑧)) = (1r𝑆))
356355adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = (1r𝑆))
357 iffalse 4437 . . . . . . . . . . . . . . 15 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
358357adantl 485 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
359356, 358eqtr4d 2839 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
360345, 347, 353, 359ifbothda 4465 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
361360mpteq2dva 5128 . . . . . . . . . . 11 (𝜑 → (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
362343, 361eqtrd 2836 . . . . . . . . . 10 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
363362adantr 484 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
364363oveq2d 7155 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺)) = (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))))
36560adantr 484 . . . . . . . . 9 ((𝜑𝑥𝐼) → 𝑇 ∈ Mnd)
366340adantlr 714 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
36728, 3ringidcl 19317 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (1r𝑆) ∈ 𝐶)
36815, 367syl 17 . . . . . . . . . . . 12 (𝜑 → (1r𝑆) ∈ 𝐶)
369368ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (1r𝑆) ∈ 𝐶)
370366, 369ifcld 4473 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ∈ 𝐶)
371370fmpttd 6860 . . . . . . . . 9 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))):𝐼𝐶)
372 eldifsnneq 4687 . . . . . . . . . . . 12 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
373372, 357syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
374373adantl 485 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
375374, 322suppss2 7851 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) supp (1r𝑆)) ⊆ {𝑥})
37650, 51, 365, 322, 324, 371, 375gsumpt 19078 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))) = ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥))
377 fveq2 6649 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
378351, 377eqtrd 2836 . . . . . . . . . 10 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑥))
379 eqid 2801 . . . . . . . . . 10 (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
380 fvex 6662 . . . . . . . . . 10 (𝐺𝑥) ∈ V
381378, 379, 380fvmpt 6749 . . . . . . . . 9 (𝑥𝐼 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
382381adantl 485 . . . . . . . 8 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
383364, 376, 3823eqtrd 2840 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺)) = (𝐺𝑥))
384335, 383oveq12d 7157 . . . . . 6 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))) = ((1r𝑆) · (𝐺𝑥)))
38528, 5, 3ringlidm 19320 . . . . . . 7 ((𝑆 ∈ Ring ∧ (𝐺𝑥) ∈ 𝐶) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
38615, 49, 385syl2an2r 684 . . . . . 6 ((𝜑𝑥𝐼) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
387384, 386eqtrd 2836 . . . . 5 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))) = (𝐺𝑥))
388326, 334, 3873eqtrd 2840 . . . 4 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐺𝑥))
389321, 388eqtrd 2836 . . 3 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐺𝑥))
390319, 254, 389eqfnfvd 6786 . 2 (𝜑 → (𝐸𝑉) = 𝐺)
391300, 314, 3903jca 1125 1 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸𝐴) = 𝐹 ∧ (𝐸𝑉) = 𝐺))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  {crab 3113  Vcvv 3444   ∖ cdif 3881   ⊆ wss 3884  ifcif 4428  {csn 4528   class class class wbr 5033   ↦ cmpt 5113   × cxp 5521  ◡ccnv 5522  ran crn 5524   “ cima 5526   ∘ ccom 5527   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139   ∘f cof 7391   ↑m cmap 8393  Fincfn 8496   finSupp cfsupp 8821  0cc0 10530  1c1 10531   + caddc 10533  ℕcn 11629  ℕ0cn0 11889  ℤcz 11973  Basecbs 16478  +gcplusg 16560  .rcmulr 16561  Scalarcsca 16563  0gc0g 16708   Σg cgsu 16709  Mndcmnd 17906   MndHom cmhm 17949  Grpcgrp 18098  .gcmg 18219   GrpHom cghm 18350  CMndccmn 18901  mulGrpcmgp 19235  1rcur 19247  Ringcrg 19293  CRingccrg 19294   RingHom crh 19463  AssAlgcasa 20542  algSccascl 20544   mVar cmvr 20593   mPoly cmpl 20594 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-ofr 7394  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12890  df-fzo 13033  df-seq 13369  df-hash 13691  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-sca 16576  df-vsca 16577  df-tset 16579  df-0g 16710  df-gsum 16711  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18101  df-minusg 18102  df-sbg 18103  df-mulg 18220  df-subg 18271  df-ghm 18351  df-cntz 18442  df-cmn 18903  df-abl 18904  df-mgp 19236  df-ur 19248  df-ring 19295  df-cring 19296  df-rnghom 19466  df-subrg 19529  df-lmod 19632  df-lss 19700  df-assa 20545  df-ascl 20547  df-psr 20597  df-mvr 20598  df-mpl 20599 This theorem is referenced by:  evlseu  20758
 Copyright terms: Public domain W3C validator