Mathbox for Steven Nguyen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  evlsbagval Structured version   Visualization version   GIF version

Theorem evlsbagval 39765
 Description: Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since 0 and 1 using 𝑈 instead of 𝑆 is convenient for its sole use case mhphf 39775, but may not be convenient for other uses. (Contributed by SN, 29-Jul-2024.)
Hypotheses
Ref Expression
evlsbagval.q 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
evlsbagval.p 𝑃 = (𝐼 mPoly 𝑈)
evlsbagval.u 𝑈 = (𝑆s 𝑅)
evlsbagval.w 𝑊 = (Base‘𝑃)
evlsbagval.k 𝐾 = (Base‘𝑆)
evlsbagval.m 𝑀 = (mulGrp‘𝑆)
evlsbagval.e = (.g𝑀)
evlsbagval.z 0 = (0g𝑈)
evlsbagval.o 1 = (1r𝑈)
evlsbagval.d 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
evlsbagval.f 𝐹 = (𝑠𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 ))
evlsbagval.i (𝜑𝐼𝑉)
evlsbagval.s (𝜑𝑆 ∈ CRing)
evlsbagval.r (𝜑𝑅 ∈ (SubRing‘𝑆))
evlsbagval.a (𝜑𝐴 ∈ (𝐾m 𝐼))
evlsbagval.b (𝜑𝐵𝐷)
Assertion
Ref Expression
evlsbagval (𝜑 → (𝐹𝑊 ∧ ((𝑄𝐹)‘𝐴) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣))))))
Distinct variable groups:   0 ,𝑠   1 ,𝑠   𝑣,𝐴   𝑣,𝐵   𝐵,   𝐵,𝑠   𝑣,𝐷   𝐷,𝑠   𝑣,𝐼   ,𝐼   𝑣,𝐾   𝑅,𝑠   𝑣,𝑆   𝑈,   𝑈,𝑠   𝜑,𝑣   𝜑,𝑠
Allowed substitution hints:   𝜑()   𝐴(,𝑠)   𝐷()   𝑃(𝑣,,𝑠)   𝑄(𝑣,,𝑠)   𝑅(𝑣,)   𝑆(,𝑠)   𝑈(𝑣)   1 (𝑣,)   (𝑣,,𝑠)   𝐹(𝑣,,𝑠)   𝐼(𝑠)   𝐾(,𝑠)   𝑀(𝑣,,𝑠)   𝑉(𝑣,,𝑠)   𝑊(𝑣,,𝑠)   0 (𝑣,)

Proof of Theorem evlsbagval
Dummy variables 𝑥 𝑔 𝑙 𝑎 𝑏 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6666 . . . . 5 (𝜑 → (Base‘𝑈) ∈ V)
2 evlsbagval.d . . . . . 6 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
3 ovexd 7178 . . . . . 6 (𝜑 → (ℕ0m 𝐼) ∈ V)
42, 3rabexd 5196 . . . . 5 (𝜑𝐷 ∈ V)
5 evlsbagval.r . . . . . . . . . 10 (𝜑𝑅 ∈ (SubRing‘𝑆))
6 evlsbagval.u . . . . . . . . . . 11 𝑈 = (𝑆s 𝑅)
76subrgring 19591 . . . . . . . . . 10 (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
85, 7syl 17 . . . . . . . . 9 (𝜑𝑈 ∈ Ring)
9 eqid 2759 . . . . . . . . . 10 (Base‘𝑈) = (Base‘𝑈)
10 evlsbagval.o . . . . . . . . . 10 1 = (1r𝑈)
119, 10ringidcl 19374 . . . . . . . . 9 (𝑈 ∈ Ring → 1 ∈ (Base‘𝑈))
128, 11syl 17 . . . . . . . 8 (𝜑1 ∈ (Base‘𝑈))
13 evlsbagval.z . . . . . . . . . 10 0 = (0g𝑈)
149, 13ring0cl 19375 . . . . . . . . 9 (𝑈 ∈ Ring → 0 ∈ (Base‘𝑈))
158, 14syl 17 . . . . . . . 8 (𝜑0 ∈ (Base‘𝑈))
1612, 15ifcld 4459 . . . . . . 7 (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
1716adantr 485 . . . . . 6 ((𝜑𝑠𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
18 evlsbagval.f . . . . . 6 𝐹 = (𝑠𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 ))
1917, 18fmptd 6862 . . . . 5 (𝜑𝐹:𝐷⟶(Base‘𝑈))
201, 4, 19elmapdd 39707 . . . 4 (𝜑𝐹 ∈ ((Base‘𝑈) ↑m 𝐷))
21 eqid 2759 . . . . 5 (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
22 eqid 2759 . . . . 5 (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
23 evlsbagval.i . . . . 5 (𝜑𝐼𝑉)
2421, 9, 2, 22, 23psrbas 20691 . . . 4 (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m 𝐷))
2520, 24eleqtrrd 2854 . . 3 (𝜑𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)))
264, 15, 18sniffsupp 8882 . . 3 (𝜑𝐹 finSupp 0 )
27 evlsbagval.p . . . 4 𝑃 = (𝐼 mPoly 𝑈)
28 evlsbagval.w . . . 4 𝑊 = (Base‘𝑃)
2927, 21, 22, 13, 28mplelbas 20743 . . 3 (𝐹𝑊 ↔ (𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ 𝐹 finSupp 0 ))
3025, 26, 29sylanbrc 587 . 2 (𝜑𝐹𝑊)
31 fveq1 6650 . . . . . . . . 9 (𝑝 = 𝐹 → (𝑝𝑏) = (𝐹𝑏))
3231fveq2d 6655 . . . . . . . 8 (𝑝 = 𝐹 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)))
3332oveq1d 7158 . . . . . . 7 (𝑝 = 𝐹 → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
3433mpteq2dv 5121 . . . . . 6 (𝑝 = 𝐹 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) = (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))
3534oveq2d 7159 . . . . 5 (𝑝 = 𝐹 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) = ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
36 evlsbagval.q . . . . . 6 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
37 evlsbagval.k . . . . . 6 𝐾 = (Base‘𝑆)
38 eqid 2759 . . . . . 6 (𝑆s (𝐾m 𝐼)) = (𝑆s (𝐾m 𝐼))
39 eqid 2759 . . . . . 6 (mulGrp‘(𝑆s (𝐾m 𝐼))) = (mulGrp‘(𝑆s (𝐾m 𝐼)))
40 eqid 2759 . . . . . 6 (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼)))) = (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))
41 eqid 2759 . . . . . 6 (.r‘(𝑆s (𝐾m 𝐼))) = (.r‘(𝑆s (𝐾m 𝐼)))
42 eqid 2759 . . . . . 6 (𝑝𝑊 ↦ ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))) = (𝑝𝑊 ↦ ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
43 eqid 2759 . . . . . 6 (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥})) = (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))
44 eqid 2759 . . . . . 6 (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))) = (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))
45 evlsbagval.s . . . . . 6 (𝜑𝑆 ∈ CRing)
4636, 27, 28, 2, 37, 6, 38, 39, 40, 41, 42, 43, 44, 23, 45, 5evlsval3 39762 . . . . 5 (𝜑𝑄 = (𝑝𝑊 ↦ ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))))
47 ovexd 7178 . . . . 5 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) ∈ V)
4835, 46, 30, 47fvmptd4 39701 . . . 4 (𝜑 → (𝑄𝐹) = ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
4948fveq1d 6653 . . 3 (𝜑 → ((𝑄𝐹)‘𝐴) = (((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))‘𝐴))
50 eqid 2759 . . . . . 6 (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (𝐾m 𝐼)))
51 eqid 2759 . . . . . 6 (0g‘(𝑆s (𝐾m 𝐼))) = (0g‘(𝑆s (𝐾m 𝐼)))
5245crngringd 19363 . . . . . . . 8 (𝜑𝑆 ∈ Ring)
53 ovexd 7178 . . . . . . . 8 (𝜑 → (𝐾m 𝐼) ∈ V)
5438pwsring 19421 . . . . . . . 8 ((𝑆 ∈ Ring ∧ (𝐾m 𝐼) ∈ V) → (𝑆s (𝐾m 𝐼)) ∈ Ring)
5552, 53, 54syl2anc 588 . . . . . . 7 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ Ring)
5655ringcmnd 39738 . . . . . 6 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ CMnd)
5755adantr 485 . . . . . . . 8 ((𝜑𝑏𝐷) → (𝑆s (𝐾m 𝐼)) ∈ Ring)
5845ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → 𝑆 ∈ CRing)
59 ovexd 7178 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → (𝐾m 𝐼) ∈ V)
6037subrgss 19589 . . . . . . . . . . . . . . 15 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐾)
615, 60syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅𝐾)
6261adantr 485 . . . . . . . . . . . . 13 ((𝜑𝑏𝐷) → 𝑅𝐾)
6362sselda 3888 . . . . . . . . . . . 12 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → 𝑥𝐾)
64 fconst6g 6546 . . . . . . . . . . . 12 (𝑥𝐾 → ((𝐾m 𝐼) × {𝑥}):(𝐾m 𝐼)⟶𝐾)
6563, 64syl 17 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → ((𝐾m 𝐼) × {𝑥}):(𝐾m 𝐼)⟶𝐾)
6638, 37, 50, 58, 59, 65pwselbasr 39758 . . . . . . . . . 10 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → ((𝐾m 𝐼) × {𝑥}) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
6766fmpttd 6863 . . . . . . . . 9 ((𝜑𝑏𝐷) → (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥})):𝑅⟶(Base‘(𝑆s (𝐾m 𝐼))))
68 eqid 2759 . . . . . . . . . . . . . . . . 17 (1r𝑆) = (1r𝑆)
696, 68subrg1 19598 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (SubRing‘𝑆) → (1r𝑆) = (1r𝑈))
705, 69syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (1r𝑆) = (1r𝑈))
7168subrg1cl 19596 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (SubRing‘𝑆) → (1r𝑆) ∈ 𝑅)
725, 71syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (1r𝑆) ∈ 𝑅)
7370, 72eqeltrrd 2852 . . . . . . . . . . . . . 14 (𝜑 → (1r𝑈) ∈ 𝑅)
7410, 73eqeltrid 2855 . . . . . . . . . . . . 13 (𝜑1𝑅)
756subrgbas 19597 . . . . . . . . . . . . . . 15 (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
765, 75syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅 = (Base‘𝑈))
7715, 76eleqtrrd 2854 . . . . . . . . . . . . 13 (𝜑0𝑅)
7874, 77ifcld 4459 . . . . . . . . . . . 12 (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
7978adantr 485 . . . . . . . . . . 11 ((𝜑𝑠𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
8079, 18fmptd 6862 . . . . . . . . . 10 (𝜑𝐹:𝐷𝑅)
8180ffvelrnda 6835 . . . . . . . . 9 ((𝜑𝑏𝐷) → (𝐹𝑏) ∈ 𝑅)
8267, 81ffvelrnd 6836 . . . . . . . 8 ((𝜑𝑏𝐷) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
8339, 50mgpbas 19298 . . . . . . . . 9 (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(mulGrp‘(𝑆s (𝐾m 𝐼))))
8438pwscrng 19423 . . . . . . . . . . . 12 ((𝑆 ∈ CRing ∧ (𝐾m 𝐼) ∈ V) → (𝑆s (𝐾m 𝐼)) ∈ CRing)
8545, 53, 84syl2anc 588 . . . . . . . . . . 11 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ CRing)
8639crngmgp 19358 . . . . . . . . . . 11 ((𝑆s (𝐾m 𝐼)) ∈ CRing → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
8785, 86syl 17 . . . . . . . . . 10 (𝜑 → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
8887adantr 485 . . . . . . . . 9 ((𝜑𝑏𝐷) → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
89 simpr 489 . . . . . . . . 9 ((𝜑𝑏𝐷) → 𝑏𝐷)
9045ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → 𝑆 ∈ CRing)
91 ovexd 7178 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → (𝐾m 𝐼) ∈ V)
92 elmapi 8431 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐾m 𝐼) → 𝑎:𝐼𝐾)
9392adantl 486 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐷) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
94 simplr 769 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐷) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
9593, 94ffvelrnd 6836 . . . . . . . . . . . 12 ((((𝜑𝑏𝐷) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
9695fmpttd 6863 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
9738, 37, 50, 90, 91, 96pwselbasr 39758 . . . . . . . . . 10 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
9897fmpttd 6863 . . . . . . . . 9 ((𝜑𝑏𝐷) → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))):𝐼⟶(Base‘(𝑆s (𝐾m 𝐼))))
992, 83, 40, 88, 89, 98psrbagev2 20825 . . . . . . . 8 ((𝜑𝑏𝐷) → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
10050, 41, 57, 82, 99ringcld 39733 . . . . . . 7 ((𝜑𝑏𝐷) → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
101100fmpttd 6863 . . . . . 6 (𝜑 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))):𝐷⟶(Base‘(𝑆s (𝐾m 𝐼))))
102 eqeq1 2763 . . . . . . . . . . . . . 14 (𝑠 = 𝑏 → (𝑠 = 𝐵𝑏 = 𝐵))
103102ifbid 4436 . . . . . . . . . . . . 13 (𝑠 = 𝑏 → if(𝑠 = 𝐵, 1 , 0 ) = if(𝑏 = 𝐵, 1 , 0 ))
104 eldifi 4028 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝐷 ∖ {𝐵}) → 𝑏𝐷)
105104adantl 486 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → 𝑏𝐷)
10610fvexi 6665 . . . . . . . . . . . . . . 15 1 ∈ V
10713fvexi 6665 . . . . . . . . . . . . . . 15 0 ∈ V
108106, 107ifex 4463 . . . . . . . . . . . . . 14 if(𝑏 = 𝐵, 1 , 0 ) ∈ V
109108a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) ∈ V)
11018, 103, 105, 109fvmptd3 6775 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹𝑏) = if(𝑏 = 𝐵, 1 , 0 ))
111 eldifsnneq 4674 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝐷 ∖ {𝐵}) → ¬ 𝑏 = 𝐵)
112111adantl 486 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ¬ 𝑏 = 𝐵)
113112iffalsed 4424 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) = 0 )
114110, 113eqtrd 2794 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹𝑏) = 0 )
115114fveq2d 6655 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 0 ))
116 sneq 4525 . . . . . . . . . . . 12 (𝑥 = 0 → {𝑥} = { 0 })
117116xpeq2d 5547 . . . . . . . . . . 11 (𝑥 = 0 → ((𝐾m 𝐼) × {𝑥}) = ((𝐾m 𝐼) × { 0 }))
11877adantr 485 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → 0𝑅)
119 ovex 7176 . . . . . . . . . . . . 13 (𝐾m 𝐼) ∈ V
120 snex 5293 . . . . . . . . . . . . 13 { 0 } ∈ V
121119, 120xpex 7467 . . . . . . . . . . . 12 ((𝐾m 𝐼) × { 0 }) ∈ V
122121a1i 11 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾m 𝐼) × { 0 }) ∈ V)
12343, 117, 118, 122fvmptd3 6775 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 0 ) = ((𝐾m 𝐼) × { 0 }))
124 eqid 2759 . . . . . . . . . . . . . . . . 17 (0g𝑆) = (0g𝑆)
1256, 124subrg0 19595 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (SubRing‘𝑆) → (0g𝑆) = (0g𝑈))
1265, 125syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0g𝑆) = (0g𝑈))
127126, 13eqtr4di 2812 . . . . . . . . . . . . . 14 (𝜑 → (0g𝑆) = 0 )
128127sneqd 4527 . . . . . . . . . . . . 13 (𝜑 → {(0g𝑆)} = { 0 })
129128xpeq2d 5547 . . . . . . . . . . . 12 (𝜑 → ((𝐾m 𝐼) × {(0g𝑆)}) = ((𝐾m 𝐼) × { 0 }))
13052ringgrpd 19359 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ Grp)
131130grpmndd 18166 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Mnd)
13238, 124pws0g 17998 . . . . . . . . . . . . 13 ((𝑆 ∈ Mnd ∧ (𝐾m 𝐼) ∈ V) → ((𝐾m 𝐼) × {(0g𝑆)}) = (0g‘(𝑆s (𝐾m 𝐼))))
133131, 53, 132syl2anc 588 . . . . . . . . . . . 12 (𝜑 → ((𝐾m 𝐼) × {(0g𝑆)}) = (0g‘(𝑆s (𝐾m 𝐼))))
134129, 133eqtr3d 2796 . . . . . . . . . . 11 (𝜑 → ((𝐾m 𝐼) × { 0 }) = (0g‘(𝑆s (𝐾m 𝐼))))
135134adantr 485 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾m 𝐼) × { 0 }) = (0g‘(𝑆s (𝐾m 𝐼))))
136115, 123, 1353eqtrd 2798 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) = (0g‘(𝑆s (𝐾m 𝐼))))
137136oveq1d 7158 . . . . . . . 8 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = ((0g‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
13887adantr 485 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
13945ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → 𝑆 ∈ CRing)
140 ovexd 7178 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → (𝐾m 𝐼) ∈ V)
14192adantl 486 . . . . . . . . . . . . . 14 ((((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
142 simplr 769 . . . . . . . . . . . . . 14 ((((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
143141, 142ffvelrnd 6836 . . . . . . . . . . . . 13 ((((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
144143fmpttd 6863 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
14538, 37, 50, 139, 140, 144pwselbasr 39758 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
146145fmpttd 6863 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))):𝐼⟶(Base‘(𝑆s (𝐾m 𝐼))))
1472, 83, 40, 138, 105, 146psrbagev2 20825 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
14850, 41, 51ringlz 19393 . . . . . . . . 9 (((𝑆s (𝐾m 𝐼)) ∈ Ring ∧ ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼)))) → ((0g‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (0g‘(𝑆s (𝐾m 𝐼))))
14955, 147, 148syl2an2r 685 . . . . . . . 8 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((0g‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (0g‘(𝑆s (𝐾m 𝐼))))
150137, 149eqtrd 2794 . . . . . . 7 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (0g‘(𝑆s (𝐾m 𝐼))))
151150, 4suppss2 7867 . . . . . 6 (𝜑 → ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) supp (0g‘(𝑆s (𝐾m 𝐼)))) ⊆ {𝐵})
1524mptexd 6971 . . . . . . 7 (𝜑 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) ∈ V)
153 fvexd 6666 . . . . . . 7 (𝜑 → (0g‘(𝑆s (𝐾m 𝐼))) ∈ V)
154 funmpt 6366 . . . . . . . 8 Fun (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
155154a1i 11 . . . . . . 7 (𝜑 → Fun (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))
156 snfi 8607 . . . . . . . . 9 {𝐵} ∈ Fin
157156a1i 11 . . . . . . . 8 (𝜑 → {𝐵} ∈ Fin)
158157, 151ssfid 8755 . . . . . . 7 (𝜑 → ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) supp (0g‘(𝑆s (𝐾m 𝐼)))) ∈ Fin)
159152, 153, 155, 158isfsuppd 39708 . . . . . 6 (𝜑 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) finSupp (0g‘(𝑆s (𝐾m 𝐼))))
16050, 51, 56, 4, 101, 151, 159gsumres 19086 . . . . 5 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) ↾ {𝐵})) = ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
161 evlsbagval.b . . . . . . . 8 (𝜑𝐵𝐷)
162161snssd 4692 . . . . . . 7 (𝜑 → {𝐵} ⊆ 𝐷)
163162resmptd 5873 . . . . . 6 (𝜑 → ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) ↾ {𝐵}) = (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))
164163oveq2d 7159 . . . . 5 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) ↾ {𝐵})) = ((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
165160, 164eqtr3d 2796 . . . 4 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) = ((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
166165fveq1d 6653 . . 3 (𝜑 → (((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))‘𝐴) = (((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))‘𝐴))
167 fveq1 6650 . . . . . . 7 (𝑔 = 𝐴 → (𝑔𝑣) = (𝐴𝑣))
168167oveq2d 7159 . . . . . 6 (𝑔 = 𝐴 → ((𝐵𝑣) (𝑔𝑣)) = ((𝐵𝑣) (𝐴𝑣)))
169168mpteq2dv 5121 . . . . 5 (𝑔 = 𝐴 → (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))) = (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣))))
170169oveq2d 7159 . . . 4 (𝑔 = 𝐴 → (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣)))) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))))
17155ringgrpd 19359 . . . . . . 7 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ Grp)
172171grpmndd 18166 . . . . . 6 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ Mnd)
173 iftrue 4419 . . . . . . . . . . . 12 (𝑠 = 𝐵 → if(𝑠 = 𝐵, 1 , 0 ) = 1 )
174106a1i 11 . . . . . . . . . . . 12 (𝜑1 ∈ V)
17518, 173, 161, 174fvmptd3 6775 . . . . . . . . . . 11 (𝜑 → (𝐹𝐵) = 1 )
176175fveq2d 6655 . . . . . . . . . 10 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 1 ))
17710, 70eqtr4id 2813 . . . . . . . . . . . 12 (𝜑1 = (1r𝑆))
178177fveq2d 6655 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 1 ) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(1r𝑆)))
179 sneq 4525 . . . . . . . . . . . . 13 (𝑥 = (1r𝑆) → {𝑥} = {(1r𝑆)})
180179xpeq2d 5547 . . . . . . . . . . . 12 (𝑥 = (1r𝑆) → ((𝐾m 𝐼) × {𝑥}) = ((𝐾m 𝐼) × {(1r𝑆)}))
181 snex 5293 . . . . . . . . . . . . . 14 {(1r𝑆)} ∈ V
182181a1i 11 . . . . . . . . . . . . 13 (𝜑 → {(1r𝑆)} ∈ V)
18353, 182xpexd 7465 . . . . . . . . . . . 12 (𝜑 → ((𝐾m 𝐼) × {(1r𝑆)}) ∈ V)
18443, 180, 72, 183fvmptd3 6775 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(1r𝑆)) = ((𝐾m 𝐼) × {(1r𝑆)}))
185178, 184eqtrd 2794 . . . . . . . . . 10 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 1 ) = ((𝐾m 𝐼) × {(1r𝑆)}))
18638, 68pws1 19422 . . . . . . . . . . 11 ((𝑆 ∈ Ring ∧ (𝐾m 𝐼) ∈ V) → ((𝐾m 𝐼) × {(1r𝑆)}) = (1r‘(𝑆s (𝐾m 𝐼))))
18752, 53, 186syl2anc 588 . . . . . . . . . 10 (𝜑 → ((𝐾m 𝐼) × {(1r𝑆)}) = (1r‘(𝑆s (𝐾m 𝐼))))
188176, 185, 1873eqtrd 2798 . . . . . . . . 9 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵)) = (1r‘(𝑆s (𝐾m 𝐼))))
189188oveq1d 7158 . . . . . . . 8 (𝜑 → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = ((1r‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
19045adantr 485 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
191 ovexd 7178 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → (𝐾m 𝐼) ∈ V)
19292adantl 486 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
193 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
194192, 193ffvelrnd 6836 . . . . . . . . . . . . 13 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
195194fmpttd 6863 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
19638, 37, 50, 190, 191, 195pwselbasr 39758 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
197196fmpttd 6863 . . . . . . . . . 10 (𝜑 → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))):𝐼⟶(Base‘(𝑆s (𝐾m 𝐼))))
1982, 83, 40, 87, 161, 197psrbagev2 20825 . . . . . . . . 9 (𝜑 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
199 eqid 2759 . . . . . . . . . 10 (1r‘(𝑆s (𝐾m 𝐼))) = (1r‘(𝑆s (𝐾m 𝐼)))
20050, 41, 199ringlidm 19377 . . . . . . . . 9 (((𝑆s (𝐾m 𝐼)) ∈ Ring ∧ ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼)))) → ((1r‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))
20155, 198, 200syl2anc 588 . . . . . . . 8 (𝜑 → ((1r‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))
202189, 201eqtrd 2794 . . . . . . 7 (𝜑 → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))
203202, 198eqeltrd 2851 . . . . . 6 (𝜑 → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
204 2fveq3 6656 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵)))
205 oveq1 7150 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))) = (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))
206205oveq2d 7159 . . . . . . . 8 (𝑏 = 𝐵 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))
207204, 206oveq12d 7161 . . . . . . 7 (𝑏 = 𝐵 → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
20850, 207gsumsn 19127 . . . . . 6 (((𝑆s (𝐾m 𝐼)) ∈ Mnd ∧ 𝐵𝐷 ∧ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) ∈ (Base‘(𝑆s (𝐾m 𝐼)))) → ((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) = (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
209172, 161, 203, 208syl3anc 1369 . . . . 5 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) = (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
2102psrbagf 20665 . . . . . . . . . . 11 (𝐵𝐷𝐵:𝐼⟶ℕ0)
211161, 210syl 17 . . . . . . . . . 10 (𝜑𝐵:𝐼⟶ℕ0)
212211ffnd 6492 . . . . . . . . 9 (𝜑𝐵 Fn 𝐼)
213119mptex 6970 . . . . . . . . . . 11 (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ V
214213, 44fnmpti 6467 . . . . . . . . . 10 (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))) Fn 𝐼
215214a1i 11 . . . . . . . . 9 (𝜑 → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))) Fn 𝐼)
216 inidm 4119 . . . . . . . . 9 (𝐼𝐼) = 𝐼
217 eqidd 2760 . . . . . . . . 9 ((𝜑𝑣𝐼) → (𝐵𝑣) = (𝐵𝑣))
218 fveq2 6651 . . . . . . . . . . 11 (𝑥 = 𝑣 → (𝑎𝑥) = (𝑎𝑣))
219218mpteq2dv 5121 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) = (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))
220 simpr 489 . . . . . . . . . 10 ((𝜑𝑣𝐼) → 𝑣𝐼)
221119mptex 6970 . . . . . . . . . . 11 (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ V
222221a1i 11 . . . . . . . . . 10 ((𝜑𝑣𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ V)
22344, 219, 220, 222fvmptd3 6775 . . . . . . . . 9 ((𝜑𝑣𝐼) → ((𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))‘𝑣) = (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))
224212, 215, 23, 23, 216, 217, 223offval 7406 . . . . . . . 8 (𝜑 → (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))) = (𝑣𝐼 ↦ ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))))
22545adantr 485 . . . . . . . . . . . 12 ((𝜑𝑣𝐼) → 𝑆 ∈ CRing)
226 ovexd 7178 . . . . . . . . . . . 12 ((𝜑𝑣𝐼) → (𝐾m 𝐼) ∈ V)
22739ringmgp 19356 . . . . . . . . . . . . . . 15 ((𝑆s (𝐾m 𝐼)) ∈ Ring → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd)
22855, 227syl 17 . . . . . . . . . . . . . 14 (𝜑 → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd)
229228adantr 485 . . . . . . . . . . . . 13 ((𝜑𝑣𝐼) → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd)
230211ffvelrnda 6835 . . . . . . . . . . . . 13 ((𝜑𝑣𝐼) → (𝐵𝑣) ∈ ℕ0)
23192adantl 486 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
232 simplr 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑣𝐼)
233231, 232ffvelrnd 6836 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑣) ∈ 𝐾)
234233fmpttd 6863 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)):(𝐾m 𝐼)⟶𝐾)
23538, 37, 50, 225, 226, 234pwselbasr 39758 . . . . . . . . . . . . 13 ((𝜑𝑣𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
23683, 40mulgnn0cl 18296 . . . . . . . . . . . . 13 (((mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd ∧ (𝐵𝑣) ∈ ℕ0 ∧ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ (Base‘(𝑆s (𝐾m 𝐼)))) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
237229, 230, 235, 236syl3anc 1369 . . . . . . . . . . . 12 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
23838, 37, 50, 225, 226, 237pwselbas 16805 . . . . . . . . . . 11 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))):(𝐾m 𝐼)⟶𝐾)
239238ffnd 6492 . . . . . . . . . 10 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) Fn (𝐾m 𝐼))
240 ovex 7176 . . . . . . . . . . . 12 ((𝐵𝑣) (𝑔𝑣)) ∈ V
241 eqid 2759 . . . . . . . . . . . 12 (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) = (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))
242240, 241fnmpti 6467 . . . . . . . . . . 11 (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) Fn (𝐾m 𝐼)
243242a1i 11 . . . . . . . . . 10 ((𝜑𝑣𝐼) → (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) Fn (𝐾m 𝐼))
244 eqid 2759 . . . . . . . . . . . . 13 (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) = (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))
245 fveq1 6650 . . . . . . . . . . . . 13 (𝑎 = 𝑙 → (𝑎𝑣) = (𝑙𝑣))
246 simpr 489 . . . . . . . . . . . . 13 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → 𝑙 ∈ (𝐾m 𝐼))
247 fvexd 6666 . . . . . . . . . . . . 13 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝑙𝑣) ∈ V)
248244, 245, 246, 247fvmptd3 6775 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))‘𝑙) = (𝑙𝑣))
249248oveq2d 7159 . . . . . . . . . . 11 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))‘𝑙)) = ((𝐵𝑣) (𝑙𝑣)))
250 evlsbagval.m . . . . . . . . . . . 12 𝑀 = (mulGrp‘𝑆)
251 evlsbagval.e . . . . . . . . . . . 12 = (.g𝑀)
25252ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → 𝑆 ∈ Ring)
253 ovexd 7178 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝐾m 𝐼) ∈ V)
254230adantr 485 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝐵𝑣) ∈ ℕ0)
255235adantr 485 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
25638, 50, 39, 250, 40, 251, 252, 253, 254, 255, 246pwsexpg 39760 . . . . . . . . . . 11 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))‘𝑙) = ((𝐵𝑣) ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))‘𝑙)))
257 fveq1 6650 . . . . . . . . . . . . 13 (𝑔 = 𝑙 → (𝑔𝑣) = (𝑙𝑣))
258257oveq2d 7159 . . . . . . . . . . . 12 (𝑔 = 𝑙 → ((𝐵𝑣) (𝑔𝑣)) = ((𝐵𝑣) (𝑙𝑣)))
259 ovexd 7178 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) (𝑙𝑣)) ∈ V)
260241, 258, 246, 259fvmptd3 6775 . . . . . . . . . . 11 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))‘𝑙) = ((𝐵𝑣) (𝑙𝑣)))
261249, 256, 2603eqtr4d 2804 . . . . . . . . . 10 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))‘𝑙) = ((𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))‘𝑙))
262239, 243, 261eqfnfvd 6789 . . . . . . . . 9 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) = (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))
263262mpteq2dva 5120 . . . . . . . 8 (𝜑 → (𝑣𝐼 ↦ ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))) = (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))))
264224, 263eqtrd 2794 . . . . . . 7 (𝜑 → (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))) = (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))))
265264oveq2d 7159 . . . . . 6 (𝜑 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))))
266250crngmgp 19358 . . . . . . . . . . 11 (𝑆 ∈ CRing → 𝑀 ∈ CMnd)
26745, 266syl 17 . . . . . . . . . 10 (𝜑𝑀 ∈ CMnd)
268267cmnmndd 18981 . . . . . . . . 9 (𝜑𝑀 ∈ Mnd)
269268adantr 485 . . . . . . . 8 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → 𝑀 ∈ Mnd)
270230adantrl 716 . . . . . . . 8 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → (𝐵𝑣) ∈ ℕ0)
271 elmapi 8431 . . . . . . . . . 10 (𝑔 ∈ (𝐾m 𝐼) → 𝑔:𝐼𝐾)
272271ad2antrl 728 . . . . . . . . 9 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → 𝑔:𝐼𝐾)
273 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → 𝑣𝐼)
274272, 273ffvelrnd 6836 . . . . . . . 8 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → (𝑔𝑣) ∈ 𝐾)
275250, 37mgpbas 19298 . . . . . . . . 9 𝐾 = (Base‘𝑀)
276275, 251mulgnn0cl 18296 . . . . . . . 8 ((𝑀 ∈ Mnd ∧ (𝐵𝑣) ∈ ℕ0 ∧ (𝑔𝑣) ∈ 𝐾) → ((𝐵𝑣) (𝑔𝑣)) ∈ 𝐾)
277269, 270, 274, 276syl3anc 1369 . . . . . . 7 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → ((𝐵𝑣) (𝑔𝑣)) ∈ 𝐾)
27823mptexd 6971 . . . . . . . 8 (𝜑 → (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) ∈ V)
279 fvexd 6666 . . . . . . . 8 (𝜑 → (1r‘(𝑆s (𝐾m 𝐼))) ∈ V)
280 funmpt 6366 . . . . . . . . 9 Fun (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))
281280a1i 11 . . . . . . . 8 (𝜑 → Fun (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))))
2822psrbagfsupp 20667 . . . . . . . . . . 11 (𝐵𝐷𝐵 finSupp 0)
283161, 282syl 17 . . . . . . . . . 10 (𝜑𝐵 finSupp 0)
284283fsuppimpd 8858 . . . . . . . . 9 (𝜑 → (𝐵 supp 0) ∈ Fin)
285 ssidd 3911 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 supp 0) ⊆ (𝐵 supp 0))
286 c0ex 10658 . . . . . . . . . . . . . . . . 17 0 ∈ V
287286a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ V)
288211, 285, 23, 287suppssr 7863 . . . . . . . . . . . . . . 15 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐵𝑣) = 0)
289288oveq1d 7158 . . . . . . . . . . . . . 14 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐵𝑣) (𝑔𝑣)) = (0 (𝑔𝑣)))
290289adantr 485 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) (𝑔𝑣)) = (0 (𝑔𝑣)))
291271adantl 486 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → 𝑔:𝐼𝐾)
292 eldifi 4028 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝐼 ∖ (𝐵 supp 0)) → 𝑣𝐼)
293292ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → 𝑣𝐼)
294291, 293ffvelrnd 6836 . . . . . . . . . . . . . 14 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → (𝑔𝑣) ∈ 𝐾)
295250, 68ringidval 19306 . . . . . . . . . . . . . . 15 (1r𝑆) = (0g𝑀)
296275, 295, 251mulg0 18283 . . . . . . . . . . . . . 14 ((𝑔𝑣) ∈ 𝐾 → (0 (𝑔𝑣)) = (1r𝑆))
297294, 296syl 17 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → (0 (𝑔𝑣)) = (1r𝑆))
298290, 297eqtrd 2794 . . . . . . . . . . . 12 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) (𝑔𝑣)) = (1r𝑆))
299298mpteq2dva 5120 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (1r𝑆)))
300 fconstmpt 5576 . . . . . . . . . . . 12 ((𝐾m 𝐼) × {(1r𝑆)}) = (𝑔 ∈ (𝐾m 𝐼) ↦ (1r𝑆))
301 ovexd 7178 . . . . . . . . . . . . 13 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐾m 𝐼) ∈ V)
30252, 301, 186syl2an2r 685 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐾m 𝐼) × {(1r𝑆)}) = (1r‘(𝑆s (𝐾m 𝐼))))
303300, 302syl5eqr 2808 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾m 𝐼) ↦ (1r𝑆)) = (1r‘(𝑆s (𝐾m 𝐼))))
304299, 303eqtrd 2794 . . . . . . . . . 10 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) = (1r‘(𝑆s (𝐾m 𝐼))))
305304, 23suppss2 7867 . . . . . . . . 9 (𝜑 → ((𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) supp (1r‘(𝑆s (𝐾m 𝐼)))) ⊆ (𝐵 supp 0))
306284, 305ssfid 8755 . . . . . . . 8 (𝜑 → ((𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) supp (1r‘(𝑆s (𝐾m 𝐼)))) ∈ Fin)
307278, 279, 281, 306isfsuppd 39708 . . . . . . 7 (𝜑 → (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) finSupp (1r‘(𝑆s (𝐾m 𝐼))))
30838, 37, 199, 39, 250, 53, 23, 45, 277, 307pwsgprod 39761 . . . . . 6 (𝜑 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
309201, 265, 3083eqtrd 2798 . . . . 5 (𝜑 → ((1r‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
310209, 189, 3093eqtrd 2798 . . . 4 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
311 evlsbagval.a . . . 4 (𝜑𝐴 ∈ (𝐾m 𝐼))
312 ovexd 7178 . . . 4 (𝜑 → (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))) ∈ V)
313170, 310, 311, 312fvmptd4 39701 . . 3 (𝜑 → (((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))‘𝐴) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))))
31449, 166, 3133eqtrd 2798 . 2 (𝜑 → ((𝑄𝐹)‘𝐴) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))))
31530, 314jca 516 1 (𝜑 → (𝐹𝑊 ∧ ((𝑄𝐹)‘𝐴) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣))))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  {crab 3072  Vcvv 3407   ∖ cdif 3851   ⊆ wss 3854  ifcif 4413  {csn 4515   class class class wbr 5025   ↦ cmpt 5105   × cxp 5515  ◡ccnv 5516   ↾ cres 5519   “ cima 5520  Fun wfun 6322   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7143   ∘f cof 7396   supp csupp 7828   ↑m cmap 8409  Fincfn 8520   finSupp cfsupp 8851  0cc0 10560  ℕcn 11659  ℕ0cn0 11919  Basecbs 16526   ↾s cress 16527  .rcmulr 16609  0gc0g 16756   Σg cgsu 16757   ↑s cpws 16763  Mndcmnd 17962  .gcmg 18276  CMndccmn 18958  mulGrpcmgp 19292  1rcur 19304  Ringcrg 19350  CRingccrg 19351  SubRingcsubrg 19584   mPwSer cmps 20651   mPoly cmpl 20653   evalSub ces 20818 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-iin 4879  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  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 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-of 7398  df-ofr 7399  df-om 7573  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-ixp 8473  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-fsupp 8852  df-sup 8924  df-oi 8992  df-card 9386  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-7 11727  df-8 11728  df-9 11729  df-n0 11920  df-z 12006  df-dec 12123  df-uz 12268  df-fz 12925  df-fzo 13068  df-seq 13404  df-hash 13726  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-sca 16624  df-vsca 16625  df-ip 16626  df-tset 16627  df-ple 16628  df-ds 16630  df-hom 16632  df-cco 16633  df-0g 16758  df-gsum 16759  df-prds 16764  df-pws 16766  df-mre 16900  df-mrc 16901  df-acs 16903  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-mhm 18007  df-submnd 18008  df-grp 18157  df-minusg 18158  df-sbg 18159  df-mulg 18277  df-subg 18328  df-ghm 18408  df-cntz 18499  df-cmn 18960  df-abl 18961  df-mgp 19293  df-ur 19305  df-srg 19309  df-ring 19352  df-cring 19353  df-rnghom 19523  df-subrg 19586  df-lmod 19689  df-lss 19757  df-lsp 19797  df-assa 20603  df-asp 20604  df-ascl 20605  df-psr 20656  df-mvr 20657  df-mpl 20658  df-evls 20820 This theorem is referenced by:  mhphf  39775
 Copyright terms: Public domain W3C validator