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

Theorem evlslem1 19730
Description: Lemma for evlseu 19731, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.)
Hypotheses
Ref Expression
evlslem1.p 𝑃 = (𝐼 mPoly 𝑅)
evlslem1.b 𝐵 = (Base‘𝑃)
evlslem1.c 𝐶 = (Base‘𝑆)
evlslem1.k 𝐾 = (Base‘𝑅)
evlslem1.d 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
evlslem1.t 𝑇 = (mulGrp‘𝑆)
evlslem1.x = (.g𝑇)
evlslem1.m · = (.r𝑆)
evlslem1.v 𝑉 = (𝐼 mVar 𝑅)
evlslem1.e 𝐸 = (𝑝𝐵 ↦ (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
evlslem1.i (𝜑𝐼 ∈ V)
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 2771 . . 3 (1r𝑃) = (1r𝑃)
3 eqid 2771 . . 3 (1r𝑆) = (1r𝑆)
4 eqid 2771 . . 3 (.r𝑃) = (.r𝑃)
5 evlslem1.m . . 3 · = (.r𝑆)
6 evlslem1.i . . . 4 (𝜑𝐼 ∈ V)
7 evlslem1.r . . . . 5 (𝜑𝑅 ∈ CRing)
8 crngring 18766 . . . . 5 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
97, 8syl 17 . . . 4 (𝜑𝑅 ∈ Ring)
10 evlslem1.p . . . . 5 𝑃 = (𝐼 mPoly 𝑅)
1110mplring 19667 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring)
126, 9, 11syl2anc 573 . . 3 (𝜑𝑃 ∈ Ring)
13 evlslem1.s . . . 4 (𝜑𝑆 ∈ CRing)
14 crngring 18766 . . . 4 (𝑆 ∈ CRing → 𝑆 ∈ Ring)
1513, 14syl 17 . . 3 (𝜑𝑆 ∈ Ring)
16 fveq2 6332 . . . . . . 7 (𝑥 = (1r𝑅) → (𝐴𝑥) = (𝐴‘(1r𝑅)))
1716fveq2d 6336 . . . . . 6 (𝑥 = (1r𝑅) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝐴‘(1r𝑅))))
18 fveq2 6332 . . . . . 6 (𝑥 = (1r𝑅) → (𝐹𝑥) = (𝐹‘(1r𝑅)))
1917, 18eqeq12d 2786 . . . . 5 (𝑥 = (1r𝑅) → ((𝐸‘(𝐴𝑥)) = (𝐹𝑥) ↔ (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅))))
20 evlslem1.d . . . . . . . . 9 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
21 eqid 2771 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
22 evlslem1.k . . . . . . . . 9 𝐾 = (Base‘𝑅)
23 evlslem1.a . . . . . . . . 9 𝐴 = (algSc‘𝑃)
246adantr 466 . . . . . . . . 9 ((𝜑𝑥𝐾) → 𝐼 ∈ V)
259adantr 466 . . . . . . . . 9 ((𝜑𝑥𝐾) → 𝑅 ∈ Ring)
26 simpr 471 . . . . . . . . 9 ((𝜑𝑥𝐾) → 𝑥𝐾)
2710, 20, 21, 22, 23, 24, 25, 26mplascl 19711 . . . . . . . 8 ((𝜑𝑥𝐾) → (𝐴𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅))))
2827fveq2d 6336 . . . . . . 7 ((𝜑𝑥𝐾) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))))
29 evlslem1.c . . . . . . . 8 𝐶 = (Base‘𝑆)
30 evlslem1.t . . . . . . . 8 𝑇 = (mulGrp‘𝑆)
31 evlslem1.x . . . . . . . 8 = (.g𝑇)
32 evlslem1.v . . . . . . . 8 𝑉 = (𝐼 mVar 𝑅)
33 evlslem1.e . . . . . . . 8 𝐸 = (𝑝𝐵 ↦ (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
347adantr 466 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝑅 ∈ CRing)
3513adantr 466 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝑆 ∈ CRing)
36 evlslem1.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
3736adantr 466 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝐹 ∈ (𝑅 RingHom 𝑆))
38 evlslem1.g . . . . . . . . 9 (𝜑𝐺:𝐼𝐶)
3938adantr 466 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝐺:𝐼𝐶)
4020psrbag0 19709 . . . . . . . . . 10 (𝐼 ∈ V → (𝐼 × {0}) ∈ 𝐷)
416, 40syl 17 . . . . . . . . 9 (𝜑 → (𝐼 × {0}) ∈ 𝐷)
4241adantr 466 . . . . . . . 8 ((𝜑𝑥𝐾) → (𝐼 × {0}) ∈ 𝐷)
4310, 1, 29, 22, 20, 30, 31, 5, 32, 33, 24, 34, 35, 37, 39, 21, 42, 26evlslem3 19729 . . . . . . 7 ((𝜑𝑥𝐾) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))) = ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺))))
44 0zd 11591 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → 0 ∈ ℤ)
45 fvexd 6344 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ V)
46 fconstmpt 5303 . . . . . . . . . . . . . . 15 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
4746a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 × {0}) = (𝑥𝐼 ↦ 0))
4838feqmptd 6391 . . . . . . . . . . . . . 14 (𝜑𝐺 = (𝑥𝐼 ↦ (𝐺𝑥)))
496, 44, 45, 47, 48offval2 7061 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 × {0}) ∘𝑓 𝐺) = (𝑥𝐼 ↦ (0 (𝐺𝑥))))
5038ffvelrnda 6502 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ 𝐶)
5130, 29mgpbas 18703 . . . . . . . . . . . . . . . 16 𝐶 = (Base‘𝑇)
5230, 3ringidval 18711 . . . . . . . . . . . . . . . 16 (1r𝑆) = (0g𝑇)
5351, 52, 31mulg0 17754 . . . . . . . . . . . . . . 15 ((𝐺𝑥) ∈ 𝐶 → (0 (𝐺𝑥)) = (1r𝑆))
5450, 53syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (0 (𝐺𝑥)) = (1r𝑆))
5554mpteq2dva 4878 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐼 ↦ (0 (𝐺𝑥))) = (𝑥𝐼 ↦ (1r𝑆)))
5649, 55eqtrd 2805 . . . . . . . . . . . 12 (𝜑 → ((𝐼 × {0}) ∘𝑓 𝐺) = (𝑥𝐼 ↦ (1r𝑆)))
5756oveq2d 6809 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺)) = (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))))
5830crngmgp 18763 . . . . . . . . . . . . . 14 (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
5913, 58syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ CMnd)
60 cmnmnd 18415 . . . . . . . . . . . . 13 (𝑇 ∈ CMnd → 𝑇 ∈ Mnd)
6159, 60syl 17 . . . . . . . . . . . 12 (𝜑𝑇 ∈ Mnd)
6252gsumz 17582 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝐼 ∈ V) → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
6361, 6, 62syl2anc 573 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
6457, 63eqtrd 2805 . . . . . . . . . 10 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺)) = (1r𝑆))
6564adantr 466 . . . . . . . . 9 ((𝜑𝑥𝐾) → (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺)) = (1r𝑆))
6665oveq2d 6809 . . . . . . . 8 ((𝜑𝑥𝐾) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺))) = ((𝐹𝑥) · (1r𝑆)))
6722, 29rhmf 18936 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾𝐶)
6836, 67syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐾𝐶)
6968ffvelrnda 6502 . . . . . . . . 9 ((𝜑𝑥𝐾) → (𝐹𝑥) ∈ 𝐶)
7029, 5, 3ringridm 18780 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ (𝐹𝑥) ∈ 𝐶) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
7115, 69, 70syl2an2r 664 . . . . . . . 8 ((𝜑𝑥𝐾) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
7266, 71eqtrd 2805 . . . . . . 7 ((𝜑𝑥𝐾) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺))) = (𝐹𝑥))
7328, 43, 723eqtrd 2809 . . . . . 6 ((𝜑𝑥𝐾) → (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
7473ralrimiva 3115 . . . . 5 (𝜑 → ∀𝑥𝐾 (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
75 eqid 2771 . . . . . . 7 (1r𝑅) = (1r𝑅)
7622, 75ringidcl 18776 . . . . . 6 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐾)
779, 76syl 17 . . . . 5 (𝜑 → (1r𝑅) ∈ 𝐾)
7819, 74, 77rspcdva 3466 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅)))
7910mplassa 19669 . . . . . . . . 9 ((𝐼 ∈ V ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
806, 7, 79syl2anc 573 . . . . . . . 8 (𝜑𝑃 ∈ AssAlg)
81 eqid 2771 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
8223, 81asclrhm 19557 . . . . . . . 8 (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
8380, 82syl 17 . . . . . . 7 (𝜑𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
8410, 6, 7mplsca 19660 . . . . . . . 8 (𝜑𝑅 = (Scalar‘𝑃))
8584oveq1d 6808 . . . . . . 7 (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
8683, 85eleqtrrd 2853 . . . . . 6 (𝜑𝐴 ∈ (𝑅 RingHom 𝑃))
8775, 2rhm1 18940 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r𝑅)) = (1r𝑃))
8886, 87syl 17 . . . . 5 (𝜑 → (𝐴‘(1r𝑅)) = (1r𝑃))
8988fveq2d 6336 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐸‘(1r𝑃)))
9075, 3rhm1 18940 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r𝑅)) = (1r𝑆))
9136, 90syl 17 . . . 4 (𝜑 → (𝐹‘(1r𝑅)) = (1r𝑆))
9278, 89, 913eqtr3d 2813 . . 3 (𝜑 → (𝐸‘(1r𝑃)) = (1r𝑆))
93 eqid 2771 . . . . 5 (+g𝑃) = (+g𝑃)
94 eqid 2771 . . . . 5 (+g𝑆) = (+g𝑆)
95 ringgrp 18760 . . . . . 6 (𝑃 ∈ Ring → 𝑃 ∈ Grp)
9612, 95syl 17 . . . . 5 (𝜑𝑃 ∈ Grp)
97 ringgrp 18760 . . . . . 6 (𝑆 ∈ Ring → 𝑆 ∈ Grp)
9815, 97syl 17 . . . . 5 (𝜑𝑆 ∈ Grp)
99 eqid 2771 . . . . . . 7 (0g𝑆) = (0g𝑆)
100 ringcmn 18789 . . . . . . . . 9 (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
10115, 100syl 17 . . . . . . . 8 (𝜑𝑆 ∈ CMnd)
102101adantr 466 . . . . . . 7 ((𝜑𝑝𝐵) → 𝑆 ∈ CMnd)
103 ovex 6823 . . . . . . . . 9 (ℕ0𝑚 𝐼) ∈ V
10420, 103rabex2 4948 . . . . . . . 8 𝐷 ∈ V
105104a1i 11 . . . . . . 7 ((𝜑𝑝𝐵) → 𝐷 ∈ V)
1066adantr 466 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐼 ∈ V)
1077adantr 466 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑅 ∈ CRing)
10813adantr 466 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑆 ∈ CRing)
10936adantr 466 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
11038adantr 466 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐺:𝐼𝐶)
111 simpr 471 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑝𝐵)
11210, 1, 29, 22, 20, 30, 31, 5, 32, 33, 106, 107, 108, 109, 110, 111evlslem6 19728 . . . . . . . 8 ((𝜑𝑝𝐵) → ((𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆)))
113112simpld 482 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶)
114112simprd 483 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆))
11529, 99, 102, 105, 113, 114gsumcl 18523 . . . . . 6 ((𝜑𝑝𝐵) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ 𝐶)
116115, 33fmptd 6527 . . . . 5 (𝜑𝐸:𝐵𝐶)
117 eqid 2771 . . . . . . . . . . . . . . . . 17 (+g𝑅) = (+g𝑅)
118 simplrl 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥𝐵)
119 simplrr 763 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦𝐵)
12010, 1, 117, 93, 118, 119mpladd 19657 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥(+g𝑃)𝑦) = (𝑥𝑓 (+g𝑅)𝑦))
121120fveq1d 6334 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑓 (+g𝑅)𝑦)‘𝑏))
122 simprl 754 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
12310, 22, 1, 20, 122mplelf 19648 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥:𝐷𝐾)
124123ffnd 6186 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 Fn 𝐷)
125124adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥 Fn 𝐷)
126 simprr 756 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
12710, 22, 1, 20, 126mplelf 19648 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦:𝐷𝐾)
128127ffnd 6186 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 Fn 𝐷)
129128adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦 Fn 𝐷)
130104a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐷 ∈ V)
131 simpr 471 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑏𝐷)
132 fnfvof 7058 . . . . . . . . . . . . . . . 16 (((𝑥 Fn 𝐷𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏𝐷)) → ((𝑥𝑓 (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
133125, 129, 130, 131, 132syl22anc 1477 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥𝑓 (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
134121, 133eqtrd 2805 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
135134fveq2d 6336 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))))
136 rhmghm 18935 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
13736, 136syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ (𝑅 GrpHom 𝑆))
138137ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
139123ffvelrnda 6502 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥𝑏) ∈ 𝐾)
140127ffvelrnda 6502 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑦𝑏) ∈ 𝐾)
14122, 117, 94ghmlin 17873 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥𝑏) ∈ 𝐾 ∧ (𝑦𝑏) ∈ 𝐾) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
142138, 139, 140, 141syl3anc 1476 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
143135, 142eqtrd 2805 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
144143oveq1d 6808 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏𝑓 𝐺))))
14515ad2antrr 705 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑆 ∈ Ring)
14668ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹:𝐾𝐶)
147146, 139ffvelrnd 6503 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑥𝑏)) ∈ 𝐶)
148146, 140ffvelrnd 6503 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑦𝑏)) ∈ 𝐶)
14959ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑇 ∈ CMnd)
15038ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐺:𝐼𝐶)
1516ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐼 ∈ V)
15220, 51, 31, 52, 149, 131, 150, 151psrbagev2 19726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑇 Σg (𝑏𝑓 𝐺)) ∈ 𝐶)
15329, 94, 5ringdir 18775 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏𝑓 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
154145, 147, 148, 152, 153syl13anc 1478 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
155144, 154eqtrd 2805 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
156155mpteq2dva 4878 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
157104a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐷 ∈ V)
158 ovexd 6825 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) ∈ V)
159 ovexd 6825 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) ∈ V)
160 eqidd 2772 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
161 eqidd 2772 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
162157, 158, 159, 160, 161offval2 7061 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
163156, 162eqtr4d 2808 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
164163oveq2d 6809 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
165101adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CMnd)
1666adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐼 ∈ V)
1677adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ CRing)
16813adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CRing)
16936adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
17038adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺:𝐼𝐶)
17110, 1, 29, 22, 20, 30, 31, 5, 32, 33, 166, 167, 168, 169, 170, 122evlslem6 19728 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆)))
172171simpld 482 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶)
17310, 1, 29, 22, 20, 30, 31, 5, 32, 33, 166, 167, 168, 169, 170, 126evlslem6 19728 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆)))
174173simpld 482 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶)
175171simprd 483 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆))
176173simprd 483 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆))
17729, 99, 94, 165, 157, 172, 174, 175, 176gsumadd 18530 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
178164, 177eqtrd 2805 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
17996adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Grp)
1801, 93grpcl 17638 . . . . . . . 8 ((𝑃 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
181179, 122, 126, 180syl3anc 1476 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
182 fveq1 6331 . . . . . . . . . . . 12 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑝𝑏) = ((𝑥(+g𝑃)𝑦)‘𝑏))
183182fveq2d 6336 . . . . . . . . . . 11 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝐹‘(𝑝𝑏)) = (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)))
184183oveq1d 6808 . . . . . . . . . 10 (𝑝 = (𝑥(+g𝑃)𝑦) → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))
185184mpteq2dv 4879 . . . . . . . . 9 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
186185oveq2d 6809 . . . . . . . 8 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
187 ovex 6823 . . . . . . . 8 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
188186, 33, 187fvmpt 6424 . . . . . . 7 ((𝑥(+g𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
189181, 188syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
190 fveq1 6331 . . . . . . . . . . . . 13 (𝑝 = 𝑥 → (𝑝𝑏) = (𝑥𝑏))
191190fveq2d 6336 . . . . . . . . . . . 12 (𝑝 = 𝑥 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑥𝑏)))
192191oveq1d 6808 . . . . . . . . . . 11 (𝑝 = 𝑥 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))
193192mpteq2dv 4879 . . . . . . . . . 10 (𝑝 = 𝑥 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
194193oveq2d 6809 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
195 ovex 6823 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
196194, 33, 195fvmpt 6424 . . . . . . . 8 (𝑥𝐵 → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
197122, 196syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
198 fveq1 6331 . . . . . . . . . . . . 13 (𝑝 = 𝑦 → (𝑝𝑏) = (𝑦𝑏))
199198fveq2d 6336 . . . . . . . . . . . 12 (𝑝 = 𝑦 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑦𝑏)))
200199oveq1d 6808 . . . . . . . . . . 11 (𝑝 = 𝑦 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))
201200mpteq2dv 4879 . . . . . . . . . 10 (𝑝 = 𝑦 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
202201oveq2d 6809 . . . . . . . . 9 (𝑝 = 𝑦 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
203 ovex 6823 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
204202, 33, 203fvmpt 6424 . . . . . . . 8 (𝑦𝐵 → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
205204ad2antll 708 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
206197, 205oveq12d 6811 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐸𝑥)(+g𝑆)(𝐸𝑦)) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
207178, 189, 2063eqtr4d 2815 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = ((𝐸𝑥)(+g𝑆)(𝐸𝑦)))
2081, 29, 93, 94, 96, 98, 116, 207isghmd 17877 . . . 4 (𝜑𝐸 ∈ (𝑃 GrpHom 𝑆))
209 eqid 2771 . . . . . . . . . . 11 (mulGrp‘𝑅) = (mulGrp‘𝑅)
210209, 30rhmmhm 18932 . . . . . . . . . 10 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
21136, 210syl 17 . . . . . . . . 9 (𝜑𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
212211adantr 466 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
213 simprll 764 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥𝐵)
21410, 22, 1, 20, 213mplelf 19648 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥:𝐷𝐾)
215 simprrl 766 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑧𝐷)
216214, 215ffvelrnd 6503 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑥𝑧) ∈ 𝐾)
217 simprlr 765 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦𝐵)
21810, 22, 1, 20, 217mplelf 19648 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦:𝐷𝐾)
219 simprrr 767 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑤𝐷)
220218, 219ffvelrnd 6503 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑦𝑤) ∈ 𝐾)
221209, 22mgpbas 18703 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
222 eqid 2771 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
223209, 222mgpplusg 18701 . . . . . . . . 9 (.r𝑅) = (+g‘(mulGrp‘𝑅))
22430, 5mgpplusg 18701 . . . . . . . . 9 · = (+g𝑇)
225221, 223, 224mhmlin 17550 . . . . . . . 8 ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥𝑧) ∈ 𝐾 ∧ (𝑦𝑤) ∈ 𝐾) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
226212, 216, 220, 225syl3anc 1476 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
22761ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → 𝑇 ∈ Mnd)
228 simprl 754 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧𝐷)
22920psrbagf 19580 . . . . . . . . . . . . . . 15 ((𝐼 ∈ V ∧ 𝑧𝐷) → 𝑧:𝐼⟶ℕ0)
2306, 228, 229syl2an2r 664 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧:𝐼⟶ℕ0)
231230ffvelrnda 6502 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) ∈ ℕ0)
232 simprr 756 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤𝐷)
23320psrbagf 19580 . . . . . . . . . . . . . . 15 ((𝐼 ∈ V ∧ 𝑤𝐷) → 𝑤:𝐼⟶ℕ0)
2346, 232, 233syl2an2r 664 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤:𝐼⟶ℕ0)
235234ffvelrnda 6502 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) ∈ ℕ0)
23638adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺:𝐼𝐶)
237236ffvelrnda 6502 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ 𝐶)
23851, 31, 224mulgnn0dir 17779 . . . . . . . . . . . . 13 ((𝑇 ∈ Mnd ∧ ((𝑧𝑣) ∈ ℕ0 ∧ (𝑤𝑣) ∈ ℕ0 ∧ (𝐺𝑣) ∈ 𝐶)) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
239227, 231, 235, 237, 238syl13anc 1478 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
240239mpteq2dva 4878 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
2416adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐼 ∈ V)
242 ovexd 6825 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) + (𝑤𝑣)) ∈ V)
243 fvexd 6344 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ V)
244230ffnd 6186 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧 Fn 𝐼)
245234ffnd 6186 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤 Fn 𝐼)
246 inidm 3971 . . . . . . . . . . . . 13 (𝐼𝐼) = 𝐼
247 eqidd 2772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) = (𝑧𝑣))
248 eqidd 2772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) = (𝑤𝑣))
249244, 245, 241, 241, 246, 247, 248offval 7051 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 + 𝑤) = (𝑣𝐼 ↦ ((𝑧𝑣) + (𝑤𝑣))))
25038feqmptd 6391 . . . . . . . . . . . . 13 (𝜑𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
251250adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
252241, 242, 243, 249, 251offval2 7061 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺) = (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))))
253 ovexd 6825 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) (𝐺𝑣)) ∈ V)
254 ovexd 6825 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑤𝑣) (𝐺𝑣)) ∈ V)
25538ffnd 6186 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐼)
256255adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 Fn 𝐼)
257 eqidd 2772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) = (𝐺𝑣))
258244, 256, 241, 241, 246, 247, 257offval 7051 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 𝐺) = (𝑣𝐼 ↦ ((𝑧𝑣) (𝐺𝑣))))
259245, 256, 241, 241, 246, 248, 257offval 7051 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤𝑓 𝐺) = (𝑣𝐼 ↦ ((𝑤𝑣) (𝐺𝑣))))
260241, 253, 254, 258, 259offval2 7061 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺)) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
261240, 252, 2603eqtr4d 2815 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺) = ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺)))
262261oveq2d 6809 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺)) = (𝑇 Σg ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺))))
26359adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑇 ∈ CMnd)
26420, 51, 31, 52, 263, 228, 236, 241psrbagev1 19725 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 𝐺):𝐼𝐶 ∧ (𝑧𝑓 𝐺) finSupp (1r𝑆)))
265264simpld 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 𝐺):𝐼𝐶)
26620, 51, 31, 52, 263, 232, 236, 241psrbagev1 19725 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑤𝑓 𝐺):𝐼𝐶 ∧ (𝑤𝑓 𝐺) finSupp (1r𝑆)))
267266simpld 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤𝑓 𝐺):𝐼𝐶)
268264simprd 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 𝐺) finSupp (1r𝑆))
269266simprd 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤𝑓 𝐺) finSupp (1r𝑆))
27051, 52, 224, 263, 241, 265, 267, 268, 269gsumadd 18530 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺))) = ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺))))
271262, 270eqtrd 2805 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺)) = ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺))))
272271adantrl 695 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺)) = ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺))))
273226, 272oveq12d 6811 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
27459adantr 466 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑇 ∈ CMnd)
27568adantr 466 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹:𝐾𝐶)
276275, 216ffvelrnd 6503 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑥𝑧)) ∈ 𝐶)
277275, 220ffvelrnd 6503 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑦𝑤)) ∈ 𝐶)
27820, 51, 31, 52, 263, 228, 236, 241psrbagev2 19726 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑧𝑓 𝐺)) ∈ 𝐶)
279278adantrl 695 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑧𝑓 𝐺)) ∈ 𝐶)
28020, 51, 31, 52, 263, 232, 236, 241psrbagev2 19726 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑤𝑓 𝐺)) ∈ 𝐶)
281280adantrl 695 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑤𝑓 𝐺)) ∈ 𝐶)
28251, 224cmn4 18419 . . . . . . 7 ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧𝑓 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤𝑓 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
283274, 276, 277, 279, 281, 282syl122anc 1485 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
284273, 283eqtrd 2805 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
2856adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐼 ∈ V)
2867adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ CRing)
28713adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑆 ∈ CRing)
28836adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
28938adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐺:𝐼𝐶)
29020psrbagaddcl 19585 . . . . . . 7 ((𝐼 ∈ V ∧ 𝑧𝐷𝑤𝐷) → (𝑧𝑓 + 𝑤) ∈ 𝐷)
291285, 215, 219, 290syl3anc 1476 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑧𝑓 + 𝑤) ∈ 𝐷)
2929adantr 466 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ Ring)
29322, 222ringcl 18769 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑥𝑧) ∈ 𝐾 ∧ (𝑦𝑤) ∈ 𝐾) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ 𝐾)
294292, 216, 220, 293syl3anc 1476 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ 𝐾)
29510, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 291, 294evlslem3 19729 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧𝑓 + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺))))
29610, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 215, 216evlslem3 19729 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) = ((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))))
29710, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 219, 220evlslem3 19729 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅)))) = ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺))))
298296, 297oveq12d 6811 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
299284, 295, 2983eqtr4d 2815 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧𝑓 + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))))
30010, 1, 5, 21, 20, 6, 7, 13, 208, 299evlslem2 19727 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(.r𝑃)𝑦)) = ((𝐸𝑥) · (𝐸𝑦)))
3011, 2, 3, 4, 5, 12, 15, 92, 300, 29, 93, 94, 116, 207isrhmd 18939 . 2 (𝜑𝐸 ∈ (𝑃 RingHom 𝑆))
302 ovex 6823 . . . . . 6 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
303302, 33fnmpti 6162 . . . . 5 𝐸 Fn 𝐵
304303a1i 11 . . . 4 (𝜑𝐸 Fn 𝐵)
30522, 1rhmf 18936 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:𝐾𝐵)
30686, 305syl 17 . . . . 5 (𝜑𝐴:𝐾𝐵)
307306ffnd 6186 . . . 4 (𝜑𝐴 Fn 𝐾)
308 frn 6193 . . . . 5 (𝐴:𝐾𝐵 → ran 𝐴𝐵)
309306, 308syl 17 . . . 4 (𝜑 → ran 𝐴𝐵)
310 fnco 6139 . . . 4 ((𝐸 Fn 𝐵𝐴 Fn 𝐾 ∧ ran 𝐴𝐵) → (𝐸𝐴) Fn 𝐾)
311304, 307, 309, 310syl3anc 1476 . . 3 (𝜑 → (𝐸𝐴) Fn 𝐾)
31268ffnd 6186 . . 3 (𝜑𝐹 Fn 𝐾)
313 fvco2 6415 . . . . 5 ((𝐴 Fn 𝐾𝑥𝐾) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
314307, 313sylan 569 . . . 4 ((𝜑𝑥𝐾) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
315314, 73eqtrd 2805 . . 3 ((𝜑𝑥𝐾) → ((𝐸𝐴)‘𝑥) = (𝐹𝑥))
316311, 312, 315eqfnfvd 6457 . 2 (𝜑 → (𝐸𝐴) = 𝐹)
31710, 32, 1, 6, 9mvrf2 19707 . . . . 5 (𝜑𝑉:𝐼𝐵)
318317ffnd 6186 . . . 4 (𝜑𝑉 Fn 𝐼)
319 frn 6193 . . . . 5 (𝑉:𝐼𝐵 → ran 𝑉𝐵)
320317, 319syl 17 . . . 4 (𝜑 → ran 𝑉𝐵)
321 fnco 6139 . . . 4 ((𝐸 Fn 𝐵𝑉 Fn 𝐼 ∧ ran 𝑉𝐵) → (𝐸𝑉) Fn 𝐼)
322304, 318, 320, 321syl3anc 1476 . . 3 (𝜑 → (𝐸𝑉) Fn 𝐼)
323 fvco2 6415 . . . . 5 ((𝑉 Fn 𝐼𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
324318, 323sylan 569 . . . 4 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
3256adantr 466 . . . . . . 7 ((𝜑𝑥𝐼) → 𝐼 ∈ V)
3267adantr 466 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑅 ∈ CRing)
327 simpr 471 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑥𝐼)
32832, 20, 21, 75, 325, 326, 327mvrval 19636 . . . . . 6 ((𝜑𝑥𝐼) → (𝑉𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅))))
329328fveq2d 6336 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))))
33013adantr 466 . . . . . 6 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
33136adantr 466 . . . . . 6 ((𝜑𝑥𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
33238adantr 466 . . . . . 6 ((𝜑𝑥𝐼) → 𝐺:𝐼𝐶)
33320psrbagsn 19710 . . . . . . . 8 (𝐼 ∈ V → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
3346, 333syl 17 . . . . . . 7 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
335334adantr 466 . . . . . 6 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
33677adantr 466 . . . . . 6 ((𝜑𝑥𝐼) → (1r𝑅) ∈ 𝐾)
33710, 1, 29, 22, 20, 30, 31, 5, 32, 33, 325, 326, 330, 331, 332, 21, 335, 336evlslem3 19729 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))) = ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺))))
33891adantr 466 . . . . . . 7 ((𝜑𝑥𝐼) → (𝐹‘(1r𝑅)) = (1r𝑆))
339 1nn0 11510 . . . . . . . . . . . . . 14 1 ∈ ℕ0
340 0nn0 11509 . . . . . . . . . . . . . 14 0 ∈ ℕ0
341339, 340keepel 4294 . . . . . . . . . . . . 13 if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
342341a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
34338ffvelrnda 6502 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
344 eqidd 2772 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
34538feqmptd 6391 . . . . . . . . . . . 12 (𝜑𝐺 = (𝑧𝐼 ↦ (𝐺𝑧)))
3466, 342, 343, 344, 345offval2 7061 . . . . . . . . . . 11 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺) = (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))))
347 oveq1 6800 . . . . . . . . . . . . . 14 (1 = if(𝑧 = 𝑥, 1, 0) → (1 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
348347eqeq1d 2773 . . . . . . . . . . . . 13 (1 = if(𝑧 = 𝑥, 1, 0) → ((1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
349 oveq1 6800 . . . . . . . . . . . . . 14 (0 = if(𝑧 = 𝑥, 1, 0) → (0 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
350349eqeq1d 2773 . . . . . . . . . . . . 13 (0 = if(𝑧 = 𝑥, 1, 0) → ((0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
351343adantr 466 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (𝐺𝑧) ∈ 𝐶)
35251, 31mulg1 17756 . . . . . . . . . . . . . . 15 ((𝐺𝑧) ∈ 𝐶 → (1 (𝐺𝑧)) = (𝐺𝑧))
353351, 352syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = (𝐺𝑧))
354 iftrue 4231 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
355354adantl 467 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
356353, 355eqtr4d 2808 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
35751, 52, 31mulg0 17754 . . . . . . . . . . . . . . . 16 ((𝐺𝑧) ∈ 𝐶 → (0 (𝐺𝑧)) = (1r𝑆))
358343, 357syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐼) → (0 (𝐺𝑧)) = (1r𝑆))
359358adantr 466 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = (1r𝑆))
360 iffalse 4234 . . . . . . . . . . . . . . 15 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
361360adantl 467 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
362359, 361eqtr4d 2808 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
363348, 350, 356, 362ifbothda 4262 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
364363mpteq2dva 4878 . . . . . . . . . . 11 (𝜑 → (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
365346, 364eqtrd 2805 . . . . . . . . . 10 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
366365adantr 466 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
367366oveq2d 6809 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺)) = (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))))
36861adantr 466 . . . . . . . . 9 ((𝜑𝑥𝐼) → 𝑇 ∈ Mnd)
369343adantlr 694 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
37029, 3ringidcl 18776 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (1r𝑆) ∈ 𝐶)
37115, 370syl 17 . . . . . . . . . . . 12 (𝜑 → (1r𝑆) ∈ 𝐶)
372371ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (1r𝑆) ∈ 𝐶)
373369, 372ifcld 4270 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ∈ 𝐶)
374 eqid 2771 . . . . . . . . . 10 (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
375373, 374fmptd 6527 . . . . . . . . 9 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))):𝐼𝐶)
376 eldifn 3884 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 ∈ {𝑥})
377 velsn 4332 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
378376, 377sylnib 317 . . . . . . . . . . . 12 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
379378, 360syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
380379adantl 467 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
381380, 325suppss2 7481 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) supp (1r𝑆)) ⊆ {𝑥})
38251, 52, 368, 325, 327, 375, 381gsumpt 18568 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))) = ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥))
383 fveq2 6332 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
384354, 383eqtrd 2805 . . . . . . . . . 10 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑥))
385 fvex 6342 . . . . . . . . . 10 (𝐺𝑥) ∈ V
386384, 374, 385fvmpt 6424 . . . . . . . . 9 (𝑥𝐼 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
387386adantl 467 . . . . . . . 8 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
388367, 382, 3873eqtrd 2809 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺)) = (𝐺𝑥))
389338, 388oveq12d 6811 . . . . . 6 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺))) = ((1r𝑆) · (𝐺𝑥)))
39029, 5, 3ringlidm 18779 . . . . . . 7 ((𝑆 ∈ Ring ∧ (𝐺𝑥) ∈ 𝐶) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
39115, 50, 390syl2an2r 664 . . . . . 6 ((𝜑𝑥𝐼) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
392389, 391eqtrd 2805 . . . . 5 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺))) = (𝐺𝑥))
393329, 337, 3923eqtrd 2809 . . . 4 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐺𝑥))
394324, 393eqtrd 2805 . . 3 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐺𝑥))
395322, 255, 394eqfnfvd 6457 . 2 (𝜑 → (𝐸𝑉) = 𝐺)
396301, 316, 3953jca 1122 1 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸𝐴) = 𝐹 ∧ (𝐸𝑉) = 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  {crab 3065  Vcvv 3351  cdif 3720  wss 3723  ifcif 4225  {csn 4316   class class class wbr 4786  cmpt 4863   × cxp 5247  ccnv 5248  ran crn 5250  cima 5252  ccom 5253   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  𝑓 cof 7042  𝑚 cmap 8009  Fincfn 8109   finSupp cfsupp 8431  0cc0 10138  1c1 10139   + caddc 10141  cn 11222  0cn0 11494  cz 11579  Basecbs 16064  +gcplusg 16149  .rcmulr 16150  Scalarcsca 16152  0gc0g 16308   Σg cgsu 16309  Mndcmnd 17502   MndHom cmhm 17541  Grpcgrp 17630  .gcmg 17748   GrpHom cghm 17865  CMndccmn 18400  mulGrpcmgp 18697  1rcur 18709  Ringcrg 18755  CRingccrg 18756   RingHom crh 18922  AssAlgcasa 19524  algSccascl 19526   mVar cmvr 19567   mPoly cmpl 19568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-ofr 7045  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534  df-fzo 12674  df-seq 13009  df-hash 13322  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-sca 16165  df-vsca 16166  df-tset 16168  df-0g 16310  df-gsum 16311  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-mhm 17543  df-submnd 17544  df-grp 17633  df-minusg 17634  df-sbg 17635  df-mulg 17749  df-subg 17799  df-ghm 17866  df-cntz 17957  df-cmn 18402  df-abl 18403  df-mgp 18698  df-ur 18710  df-ring 18757  df-cring 18758  df-rnghom 18925  df-subrg 18988  df-lmod 19075  df-lss 19143  df-assa 19527  df-ascl 19529  df-psr 19571  df-mvr 19572  df-mpl 19573
This theorem is referenced by:  evlseu  19731
  Copyright terms: Public domain W3C validator