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

Theorem evlsbagval 40736
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 40757, 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 6857 . . . . 5 (𝜑 → (Base‘𝑈) ∈ V)
2 evlsbagval.d . . . . . 6 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
3 ovexd 7392 . . . . . 6 (𝜑 → (ℕ0m 𝐼) ∈ V)
42, 3rabexd 5290 . . . . 5 (𝜑𝐷 ∈ V)
5 evlsbagval.r . . . . . . . . . 10 (𝜑𝑅 ∈ (SubRing‘𝑆))
6 evlsbagval.u . . . . . . . . . . 11 𝑈 = (𝑆s 𝑅)
76subrgring 20225 . . . . . . . . . 10 (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
85, 7syl 17 . . . . . . . . 9 (𝜑𝑈 ∈ Ring)
9 eqid 2736 . . . . . . . . . 10 (Base‘𝑈) = (Base‘𝑈)
10 evlsbagval.o . . . . . . . . . 10 1 = (1r𝑈)
119, 10ringidcl 19989 . . . . . . . . 9 (𝑈 ∈ Ring → 1 ∈ (Base‘𝑈))
128, 11syl 17 . . . . . . . 8 (𝜑1 ∈ (Base‘𝑈))
13 evlsbagval.z . . . . . . . . . 10 0 = (0g𝑈)
149, 13ring0cl 19990 . . . . . . . . 9 (𝑈 ∈ Ring → 0 ∈ (Base‘𝑈))
158, 14syl 17 . . . . . . . 8 (𝜑0 ∈ (Base‘𝑈))
1612, 15ifcld 4532 . . . . . . 7 (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
1716adantr 481 . . . . . 6 ((𝜑𝑠𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
18 evlsbagval.f . . . . . 6 𝐹 = (𝑠𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 ))
1917, 18fmptd 7062 . . . . 5 (𝜑𝐹:𝐷⟶(Base‘𝑈))
201, 4, 19elmapdd 40664 . . . 4 (𝜑𝐹 ∈ ((Base‘𝑈) ↑m 𝐷))
21 eqid 2736 . . . . 5 (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
22 eqid 2736 . . . . 5 (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
23 evlsbagval.i . . . . 5 (𝜑𝐼𝑉)
2421, 9, 2, 22, 23psrbas 21346 . . . 4 (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m 𝐷))
2520, 24eleqtrrd 2841 . . 3 (𝜑𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)))
264, 15, 18sniffsupp 9336 . . 3 (𝜑𝐹 finSupp 0 )
27 evlsbagval.p . . . 4 𝑃 = (𝐼 mPoly 𝑈)
28 evlsbagval.w . . . 4 𝑊 = (Base‘𝑃)
2927, 21, 22, 13, 28mplelbas 21399 . . 3 (𝐹𝑊 ↔ (𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ 𝐹 finSupp 0 ))
3025, 26, 29sylanbrc 583 . 2 (𝜑𝐹𝑊)
31 fveq1 6841 . . . . . 6 (𝑔 = 𝐴 → (𝑔𝑣) = (𝐴𝑣))
3231oveq2d 7373 . . . . 5 (𝑔 = 𝐴 → ((𝐵𝑣) (𝑔𝑣)) = ((𝐵𝑣) (𝐴𝑣)))
3332mpteq2dv 5207 . . . 4 (𝑔 = 𝐴 → (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))) = (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣))))
3433oveq2d 7373 . . 3 (𝑔 = 𝐴 → (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣)))) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))))
35 fveq1 6841 . . . . . . . . 9 (𝑝 = 𝐹 → (𝑝𝑏) = (𝐹𝑏))
3635fveq2d 6846 . . . . . . . 8 (𝑝 = 𝐹 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)))
3736oveq1d 7372 . . . . . . 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 𝐼) ↦ (𝑎𝑥)))))))
3837mpteq2dv 5207 . . . . . 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 𝐼) ↦ (𝑎𝑥))))))))
3938oveq2d 7373 . . . . 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 𝐼) ↦ (𝑎𝑥)))))))))
40 evlsbagval.q . . . . . 6 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
41 evlsbagval.k . . . . . 6 𝐾 = (Base‘𝑆)
42 eqid 2736 . . . . . 6 (𝑆s (𝐾m 𝐼)) = (𝑆s (𝐾m 𝐼))
43 eqid 2736 . . . . . 6 (mulGrp‘(𝑆s (𝐾m 𝐼))) = (mulGrp‘(𝑆s (𝐾m 𝐼)))
44 eqid 2736 . . . . . 6 (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼)))) = (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))
45 eqid 2736 . . . . . 6 (.r‘(𝑆s (𝐾m 𝐼))) = (.r‘(𝑆s (𝐾m 𝐼)))
46 eqid 2736 . . . . . 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 𝐼) ↦ (𝑎𝑥)))))))))
47 eqid 2736 . . . . . 6 (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥})) = (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))
48 eqid 2736 . . . . . 6 (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))) = (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))
49 evlsbagval.s . . . . . 6 (𝜑𝑆 ∈ CRing)
5040, 27, 28, 2, 41, 6, 42, 43, 44, 45, 46, 47, 48, 23, 49, 5evlsval3 40732 . . . . 5 (𝜑𝑄 = (𝑝𝑊 ↦ ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝑝𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))))
51 ovexd 7392 . . . . 5 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) ∈ V)
5239, 50, 30, 51fvmptd4 40658 . . . 4 (𝜑 → (𝑄𝐹) = ((𝑆s (𝐾m 𝐼)) Σg (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))))
53 eqid 2736 . . . . . 6 (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (𝐾m 𝐼)))
54 eqid 2736 . . . . . 6 (0g‘(𝑆s (𝐾m 𝐼))) = (0g‘(𝑆s (𝐾m 𝐼)))
5549crngringd 19977 . . . . . . . 8 (𝜑𝑆 ∈ Ring)
56 ovexd 7392 . . . . . . . 8 (𝜑 → (𝐾m 𝐼) ∈ V)
5742pwsring 20039 . . . . . . . 8 ((𝑆 ∈ Ring ∧ (𝐾m 𝐼) ∈ V) → (𝑆s (𝐾m 𝐼)) ∈ Ring)
5855, 56, 57syl2anc 584 . . . . . . 7 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ Ring)
5958ringcmnd 20005 . . . . . 6 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ CMnd)
6058adantr 481 . . . . . . . 8 ((𝜑𝑏𝐷) → (𝑆s (𝐾m 𝐼)) ∈ Ring)
6149ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → 𝑆 ∈ CRing)
62 ovexd 7392 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → (𝐾m 𝐼) ∈ V)
6341subrgss 20223 . . . . . . . . . . . . . . 15 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐾)
645, 63syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅𝐾)
6564adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑏𝐷) → 𝑅𝐾)
6665sselda 3944 . . . . . . . . . . . 12 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → 𝑥𝐾)
67 fconst6g 6731 . . . . . . . . . . . 12 (𝑥𝐾 → ((𝐾m 𝐼) × {𝑥}):(𝐾m 𝐼)⟶𝐾)
6866, 67syl 17 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → ((𝐾m 𝐼) × {𝑥}):(𝐾m 𝐼)⟶𝐾)
6942, 41, 53, 61, 62, 68pwselbasr 40719 . . . . . . . . . 10 (((𝜑𝑏𝐷) ∧ 𝑥𝑅) → ((𝐾m 𝐼) × {𝑥}) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
7069fmpttd 7063 . . . . . . . . 9 ((𝜑𝑏𝐷) → (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥})):𝑅⟶(Base‘(𝑆s (𝐾m 𝐼))))
71 eqid 2736 . . . . . . . . . . . . . . . . 17 (1r𝑆) = (1r𝑆)
726, 71subrg1 20232 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (SubRing‘𝑆) → (1r𝑆) = (1r𝑈))
735, 72syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (1r𝑆) = (1r𝑈))
7471subrg1cl 20230 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (SubRing‘𝑆) → (1r𝑆) ∈ 𝑅)
755, 74syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (1r𝑆) ∈ 𝑅)
7673, 75eqeltrrd 2839 . . . . . . . . . . . . . 14 (𝜑 → (1r𝑈) ∈ 𝑅)
7710, 76eqeltrid 2842 . . . . . . . . . . . . 13 (𝜑1𝑅)
786subrgbas 20231 . . . . . . . . . . . . . . 15 (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
795, 78syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅 = (Base‘𝑈))
8015, 79eleqtrrd 2841 . . . . . . . . . . . . 13 (𝜑0𝑅)
8177, 80ifcld 4532 . . . . . . . . . . . 12 (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
8281adantr 481 . . . . . . . . . . 11 ((𝜑𝑠𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
8382, 18fmptd 7062 . . . . . . . . . 10 (𝜑𝐹:𝐷𝑅)
8483ffvelcdmda 7035 . . . . . . . . 9 ((𝜑𝑏𝐷) → (𝐹𝑏) ∈ 𝑅)
8570, 84ffvelcdmd 7036 . . . . . . . 8 ((𝜑𝑏𝐷) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
8643, 53mgpbas 19902 . . . . . . . . 9 (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(mulGrp‘(𝑆s (𝐾m 𝐼))))
8742pwscrng 20041 . . . . . . . . . . . 12 ((𝑆 ∈ CRing ∧ (𝐾m 𝐼) ∈ V) → (𝑆s (𝐾m 𝐼)) ∈ CRing)
8849, 56, 87syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ CRing)
8943crngmgp 19972 . . . . . . . . . . 11 ((𝑆s (𝐾m 𝐼)) ∈ CRing → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
9088, 89syl 17 . . . . . . . . . 10 (𝜑 → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
9190adantr 481 . . . . . . . . 9 ((𝜑𝑏𝐷) → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
92 simpr 485 . . . . . . . . 9 ((𝜑𝑏𝐷) → 𝑏𝐷)
9349ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → 𝑆 ∈ CRing)
94 ovexd 7392 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → (𝐾m 𝐼) ∈ V)
95 elmapi 8787 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐾m 𝐼) → 𝑎:𝐼𝐾)
9695adantl 482 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐷) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
97 simplr 767 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐷) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
9896, 97ffvelcdmd 7036 . . . . . . . . . . . 12 ((((𝜑𝑏𝐷) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
9998fmpttd 7063 . . . . . . . . . . 11 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
10042, 41, 53, 93, 94, 99pwselbasr 40719 . . . . . . . . . 10 (((𝜑𝑏𝐷) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
101100fmpttd 7063 . . . . . . . . 9 ((𝜑𝑏𝐷) → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))):𝐼⟶(Base‘(𝑆s (𝐾m 𝐼))))
1022, 86, 44, 91, 92, 101psrbagev2 21487 . . . . . . . 8 ((𝜑𝑏𝐷) → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
10353, 45, 60, 85, 102ringcld 19986 . . . . . . 7 ((𝜑𝑏𝐷) → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
104103fmpttd 7063 . . . . . 6 (𝜑 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))):𝐷⟶(Base‘(𝑆s (𝐾m 𝐼))))
105 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑠 = 𝑏 → (𝑠 = 𝐵𝑏 = 𝐵))
106105ifbid 4509 . . . . . . . . . . . . 13 (𝑠 = 𝑏 → if(𝑠 = 𝐵, 1 , 0 ) = if(𝑏 = 𝐵, 1 , 0 ))
107 eldifi 4086 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝐷 ∖ {𝐵}) → 𝑏𝐷)
108107adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → 𝑏𝐷)
10910fvexi 6856 . . . . . . . . . . . . . . 15 1 ∈ V
11013fvexi 6856 . . . . . . . . . . . . . . 15 0 ∈ V
111109, 110ifex 4536 . . . . . . . . . . . . . 14 if(𝑏 = 𝐵, 1 , 0 ) ∈ V
112111a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) ∈ V)
11318, 106, 108, 112fvmptd3 6971 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹𝑏) = if(𝑏 = 𝐵, 1 , 0 ))
114 eldifsnneq 4751 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝐷 ∖ {𝐵}) → ¬ 𝑏 = 𝐵)
115114adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ¬ 𝑏 = 𝐵)
116115iffalsed 4497 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) = 0 )
117113, 116eqtrd 2776 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹𝑏) = 0 )
118117fveq2d 6846 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 0 ))
119 sneq 4596 . . . . . . . . . . . 12 (𝑥 = 0 → {𝑥} = { 0 })
120119xpeq2d 5663 . . . . . . . . . . 11 (𝑥 = 0 → ((𝐾m 𝐼) × {𝑥}) = ((𝐾m 𝐼) × { 0 }))
12180adantr 481 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → 0𝑅)
122 ovex 7390 . . . . . . . . . . . . 13 (𝐾m 𝐼) ∈ V
123 snex 5388 . . . . . . . . . . . . 13 { 0 } ∈ V
124122, 123xpex 7687 . . . . . . . . . . . 12 ((𝐾m 𝐼) × { 0 }) ∈ V
125124a1i 11 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾m 𝐼) × { 0 }) ∈ V)
12647, 120, 121, 125fvmptd3 6971 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 0 ) = ((𝐾m 𝐼) × { 0 }))
127 eqid 2736 . . . . . . . . . . . . . . . . 17 (0g𝑆) = (0g𝑆)
1286, 127subrg0 20229 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (SubRing‘𝑆) → (0g𝑆) = (0g𝑈))
1295, 128syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0g𝑆) = (0g𝑈))
130129, 13eqtr4di 2794 . . . . . . . . . . . . . 14 (𝜑 → (0g𝑆) = 0 )
131130sneqd 4598 . . . . . . . . . . . . 13 (𝜑 → {(0g𝑆)} = { 0 })
132131xpeq2d 5663 . . . . . . . . . . . 12 (𝜑 → ((𝐾m 𝐼) × {(0g𝑆)}) = ((𝐾m 𝐼) × { 0 }))
13355ringgrpd 19973 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ Grp)
134133grpmndd 18760 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Mnd)
13542, 127pws0g 18592 . . . . . . . . . . . . 13 ((𝑆 ∈ Mnd ∧ (𝐾m 𝐼) ∈ V) → ((𝐾m 𝐼) × {(0g𝑆)}) = (0g‘(𝑆s (𝐾m 𝐼))))
136134, 56, 135syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝐾m 𝐼) × {(0g𝑆)}) = (0g‘(𝑆s (𝐾m 𝐼))))
137132, 136eqtr3d 2778 . . . . . . . . . . 11 (𝜑 → ((𝐾m 𝐼) × { 0 }) = (0g‘(𝑆s (𝐾m 𝐼))))
138137adantr 481 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾m 𝐼) × { 0 }) = (0g‘(𝑆s (𝐾m 𝐼))))
139118, 126, 1383eqtrd 2780 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) = (0g‘(𝑆s (𝐾m 𝐼))))
140139oveq1d 7372 . . . . . . . 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 𝐼) ↦ (𝑎𝑥)))))))
14190adantr 481 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ CMnd)
14249ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → 𝑆 ∈ CRing)
143 ovexd 7392 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → (𝐾m 𝐼) ∈ V)
14495adantl 482 . . . . . . . . . . . . . 14 ((((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
145 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
146144, 145ffvelcdmd 7036 . . . . . . . . . . . . 13 ((((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
147146fmpttd 7063 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
14842, 41, 53, 142, 143, 147pwselbasr 40719 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
149148fmpttd 7063 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))):𝐼⟶(Base‘(𝑆s (𝐾m 𝐼))))
1502, 86, 44, 141, 108, 149psrbagev2 21487 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
15153, 45, 54ringlz 20011 . . . . . . . . 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 𝐼))))
15258, 150, 151syl2an2r 683 . . . . . . . 8 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → ((0g‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (0g‘(𝑆s (𝐾m 𝐼))))
153140, 152eqtrd 2776 . . . . . . 7 ((𝜑𝑏 ∈ (𝐷 ∖ {𝐵})) → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (0g‘(𝑆s (𝐾m 𝐼))))
154153, 4suppss2 8131 . . . . . 6 (𝜑 → ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) supp (0g‘(𝑆s (𝐾m 𝐼)))) ⊆ {𝐵})
1554mptexd 7174 . . . . . . 7 (𝜑 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) ∈ V)
156 fvexd 6857 . . . . . . 7 (𝜑 → (0g‘(𝑆s (𝐾m 𝐼))) ∈ V)
157 funmpt 6539 . . . . . . . 8 Fun (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))
158157a1i 11 . . . . . . 7 (𝜑 → Fun (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))))
159 snfi 8988 . . . . . . . . 9 {𝐵} ∈ Fin
160159a1i 11 . . . . . . . 8 (𝜑 → {𝐵} ∈ Fin)
161160, 154ssfid 9211 . . . . . . 7 (𝜑 → ((𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) supp (0g‘(𝑆s (𝐾m 𝐼)))) ∈ Fin)
162155, 156, 158, 161isfsuppd 40665 . . . . . 6 (𝜑 → (𝑏𝐷 ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))) finSupp (0g‘(𝑆s (𝐾m 𝐼))))
16353, 54, 59, 4, 104, 154, 162gsumres 19690 . . . . 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 𝐼) ↦ (𝑎𝑥)))))))))
164 evlsbagval.b . . . . . . . 8 (𝜑𝐵𝐷)
165164snssd 4769 . . . . . . 7 (𝜑 → {𝐵} ⊆ 𝐷)
166165resmptd 5994 . . . . . 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 𝐼) ↦ (𝑎𝑥))))))))
167166oveq2d 7373 . . . . 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 𝐼) ↦ (𝑎𝑥)))))))))
168163, 167eqtr3d 2778 . . . 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 𝐼) ↦ (𝑎𝑥)))))))))
16958ringgrpd 19973 . . . . . . 7 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ Grp)
170169grpmndd 18760 . . . . . 6 (𝜑 → (𝑆s (𝐾m 𝐼)) ∈ Mnd)
171 iftrue 4492 . . . . . . . . . . . 12 (𝑠 = 𝐵 → if(𝑠 = 𝐵, 1 , 0 ) = 1 )
172109a1i 11 . . . . . . . . . . . 12 (𝜑1 ∈ V)
17318, 171, 164, 172fvmptd3 6971 . . . . . . . . . . 11 (𝜑 → (𝐹𝐵) = 1 )
174173fveq2d 6846 . . . . . . . . . 10 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 1 ))
17510, 73eqtr4id 2795 . . . . . . . . . . . 12 (𝜑1 = (1r𝑆))
176175fveq2d 6846 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 1 ) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(1r𝑆)))
177 sneq 4596 . . . . . . . . . . . . 13 (𝑥 = (1r𝑆) → {𝑥} = {(1r𝑆)})
178177xpeq2d 5663 . . . . . . . . . . . 12 (𝑥 = (1r𝑆) → ((𝐾m 𝐼) × {𝑥}) = ((𝐾m 𝐼) × {(1r𝑆)}))
179 snex 5388 . . . . . . . . . . . . . 14 {(1r𝑆)} ∈ V
180179a1i 11 . . . . . . . . . . . . 13 (𝜑 → {(1r𝑆)} ∈ V)
18156, 180xpexd 7685 . . . . . . . . . . . 12 (𝜑 → ((𝐾m 𝐼) × {(1r𝑆)}) ∈ V)
18247, 178, 75, 181fvmptd3 6971 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(1r𝑆)) = ((𝐾m 𝐼) × {(1r𝑆)}))
183176, 182eqtrd 2776 . . . . . . . . . 10 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘ 1 ) = ((𝐾m 𝐼) × {(1r𝑆)}))
18442, 71pws1 20040 . . . . . . . . . . 11 ((𝑆 ∈ Ring ∧ (𝐾m 𝐼) ∈ V) → ((𝐾m 𝐼) × {(1r𝑆)}) = (1r‘(𝑆s (𝐾m 𝐼))))
18555, 56, 184syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝐾m 𝐼) × {(1r𝑆)}) = (1r‘(𝑆s (𝐾m 𝐼))))
186174, 183, 1853eqtrd 2780 . . . . . . . . 9 (𝜑 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵)) = (1r‘(𝑆s (𝐾m 𝐼))))
187186oveq1d 7372 . . . . . . . 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 𝐼) ↦ (𝑎𝑥)))))))
188 eqid 2736 . . . . . . . . 9 (1r‘(𝑆s (𝐾m 𝐼))) = (1r‘(𝑆s (𝐾m 𝐼)))
18949adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
190 ovexd 7392 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → (𝐾m 𝐼) ∈ V)
19195adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
192 simplr 767 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
193191, 192ffvelcdmd 7036 . . . . . . . . . . . . 13 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
194193fmpttd 7063 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
19542, 41, 53, 189, 190, 194pwselbasr 40719 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
196195fmpttd 7063 . . . . . . . . . 10 (𝜑 → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))):𝐼⟶(Base‘(𝑆s (𝐾m 𝐼))))
1972, 86, 44, 90, 164, 196psrbagev2 21487 . . . . . . . . 9 (𝜑 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
19853, 45, 188, 58, 197ringlidmd 40691 . . . . . . . 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 𝐼) ↦ (𝑎𝑥))))))
199187, 198eqtrd 2776 . . . . . . 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 𝐼) ↦ (𝑎𝑥))))))
200199, 197eqeltrd 2838 . . . . . 6 (𝜑 → (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
201 2fveq3 6847 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏)) = ((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝐵)))
202 oveq1 7364 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))) = (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))
203202oveq2d 7373 . . . . . . . 8 (𝑏 = 𝐵 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))))
204201, 203oveq12d 7375 . . . . . . 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 𝐼) ↦ (𝑎𝑥)))))))
20553, 204gsumsn 19731 . . . . . 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 𝐼) ↦ (𝑎𝑥)))))))
206170, 164, 200, 205syl3anc 1371 . . . . 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 𝐼) ↦ (𝑎𝑥)))))))
2072psrbagf 21320 . . . . . . . . . . 11 (𝐵𝐷𝐵:𝐼⟶ℕ0)
208164, 207syl 17 . . . . . . . . . 10 (𝜑𝐵:𝐼⟶ℕ0)
209208ffnd 6669 . . . . . . . . 9 (𝜑𝐵 Fn 𝐼)
210122mptex 7173 . . . . . . . . . . 11 (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ V
211210, 48fnmpti 6644 . . . . . . . . . 10 (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))) Fn 𝐼
212211a1i 11 . . . . . . . . 9 (𝜑 → (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))) Fn 𝐼)
213 inidm 4178 . . . . . . . . 9 (𝐼𝐼) = 𝐼
214 eqidd 2737 . . . . . . . . 9 ((𝜑𝑣𝐼) → (𝐵𝑣) = (𝐵𝑣))
215 fveq2 6842 . . . . . . . . . . 11 (𝑥 = 𝑣 → (𝑎𝑥) = (𝑎𝑣))
216215mpteq2dv 5207 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) = (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))
217 simpr 485 . . . . . . . . . 10 ((𝜑𝑣𝐼) → 𝑣𝐼)
218122mptex 7173 . . . . . . . . . . 11 (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ V
219218a1i 11 . . . . . . . . . 10 ((𝜑𝑣𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ V)
22048, 216, 217, 219fvmptd3 6971 . . . . . . . . 9 ((𝜑𝑣𝐼) → ((𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))‘𝑣) = (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))
221209, 212, 23, 23, 213, 214, 220offval 7626 . . . . . . . 8 (𝜑 → (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))) = (𝑣𝐼 ↦ ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))))
22249adantr 481 . . . . . . . . . . . 12 ((𝜑𝑣𝐼) → 𝑆 ∈ CRing)
223 ovexd 7392 . . . . . . . . . . . 12 ((𝜑𝑣𝐼) → (𝐾m 𝐼) ∈ V)
22443ringmgp 19970 . . . . . . . . . . . . . . 15 ((𝑆s (𝐾m 𝐼)) ∈ Ring → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd)
22558, 224syl 17 . . . . . . . . . . . . . 14 (𝜑 → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd)
226225adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑣𝐼) → (mulGrp‘(𝑆s (𝐾m 𝐼))) ∈ Mnd)
227208ffvelcdmda 7035 . . . . . . . . . . . . 13 ((𝜑𝑣𝐼) → (𝐵𝑣) ∈ ℕ0)
22895adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
229 simplr 767 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑣𝐼)
230228, 229ffvelcdmd 7036 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑣) ∈ 𝐾)
231230fmpttd 7063 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)):(𝐾m 𝐼)⟶𝐾)
23242, 41, 53, 222, 223, 231pwselbasr 40719 . . . . . . . . . . . . 13 ((𝜑𝑣𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
23386, 44, 226, 227, 232mulgnn0cld 18897 . . . . . . . . . . . 12 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
23442, 41, 53, 222, 223, 233pwselbas 17371 . . . . . . . . . . 11 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))):(𝐾m 𝐼)⟶𝐾)
235234ffnd 6669 . . . . . . . . . 10 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) Fn (𝐾m 𝐼))
236 ovex 7390 . . . . . . . . . . . 12 ((𝐵𝑣) (𝑔𝑣)) ∈ V
237 eqid 2736 . . . . . . . . . . . 12 (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) = (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))
238236, 237fnmpti 6644 . . . . . . . . . . 11 (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) Fn (𝐾m 𝐼)
239238a1i 11 . . . . . . . . . 10 ((𝜑𝑣𝐼) → (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) Fn (𝐾m 𝐼))
240 eqid 2736 . . . . . . . . . . . . 13 (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) = (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))
241 fveq1 6841 . . . . . . . . . . . . 13 (𝑎 = 𝑙 → (𝑎𝑣) = (𝑙𝑣))
242 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → 𝑙 ∈ (𝐾m 𝐼))
243 fvexd 6857 . . . . . . . . . . . . 13 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝑙𝑣) ∈ V)
244240, 241, 242, 243fvmptd3 6971 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))‘𝑙) = (𝑙𝑣))
245244oveq2d 7373 . . . . . . . . . . 11 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))‘𝑙)) = ((𝐵𝑣) (𝑙𝑣)))
246 evlsbagval.m . . . . . . . . . . . 12 𝑀 = (mulGrp‘𝑆)
247 evlsbagval.e . . . . . . . . . . . 12 = (.g𝑀)
24855ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → 𝑆 ∈ Ring)
249 ovexd 7392 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝐾m 𝐼) ∈ V)
250227adantr 481 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝐵𝑣) ∈ ℕ0)
251232adantr 481 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
25242, 53, 43, 246, 44, 247, 248, 249, 250, 251, 242pwsexpg 20044 . . . . . . . . . . 11 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))‘𝑙) = ((𝐵𝑣) ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))‘𝑙)))
253 fveq1 6841 . . . . . . . . . . . . 13 (𝑔 = 𝑙 → (𝑔𝑣) = (𝑙𝑣))
254253oveq2d 7373 . . . . . . . . . . . 12 (𝑔 = 𝑙 → ((𝐵𝑣) (𝑔𝑣)) = ((𝐵𝑣) (𝑙𝑣)))
255 ovexd 7392 . . . . . . . . . . . 12 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) (𝑙𝑣)) ∈ V)
256237, 254, 242, 255fvmptd3 6971 . . . . . . . . . . 11 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → ((𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))‘𝑙) = ((𝐵𝑣) (𝑙𝑣)))
257245, 252, 2563eqtr4d 2786 . . . . . . . . . 10 (((𝜑𝑣𝐼) ∧ 𝑙 ∈ (𝐾m 𝐼)) → (((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))‘𝑙) = ((𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))‘𝑙))
258235, 239, 257eqfnfvd 6985 . . . . . . . . 9 ((𝜑𝑣𝐼) → ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣))) = (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))
259258mpteq2dva 5205 . . . . . . . 8 (𝜑 → (𝑣𝐼 ↦ ((𝐵𝑣)(.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑣)))) = (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))))
260221, 259eqtrd 2776 . . . . . . 7 (𝜑 → (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))) = (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))))
261260oveq2d 7373 . . . . . 6 (𝜑 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥))))) = ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))))
262246, 41mgpbas 19902 . . . . . . . 8 𝐾 = (Base‘𝑀)
263246crngmgp 19972 . . . . . . . . . . 11 (𝑆 ∈ CRing → 𝑀 ∈ CMnd)
26449, 263syl 17 . . . . . . . . . 10 (𝜑𝑀 ∈ CMnd)
265264cmnmndd 19586 . . . . . . . . 9 (𝜑𝑀 ∈ Mnd)
266265adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → 𝑀 ∈ Mnd)
267227adantrl 714 . . . . . . . 8 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → (𝐵𝑣) ∈ ℕ0)
268 elmapi 8787 . . . . . . . . . 10 (𝑔 ∈ (𝐾m 𝐼) → 𝑔:𝐼𝐾)
269268ad2antrl 726 . . . . . . . . 9 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → 𝑔:𝐼𝐾)
270 simprr 771 . . . . . . . . 9 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → 𝑣𝐼)
271269, 270ffvelcdmd 7036 . . . . . . . 8 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → (𝑔𝑣) ∈ 𝐾)
272262, 247, 266, 267, 271mulgnn0cld 18897 . . . . . . 7 ((𝜑 ∧ (𝑔 ∈ (𝐾m 𝐼) ∧ 𝑣𝐼)) → ((𝐵𝑣) (𝑔𝑣)) ∈ 𝐾)
27323mptexd 7174 . . . . . . . 8 (𝜑 → (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) ∈ V)
274 fvexd 6857 . . . . . . . 8 (𝜑 → (1r‘(𝑆s (𝐾m 𝐼))) ∈ V)
275 funmpt 6539 . . . . . . . . 9 Fun (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))
276275a1i 11 . . . . . . . 8 (𝜑 → Fun (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))))
2772psrbagfsupp 21322 . . . . . . . . . . 11 (𝐵𝐷𝐵 finSupp 0)
278164, 277syl 17 . . . . . . . . . 10 (𝜑𝐵 finSupp 0)
279278fsuppimpd 9312 . . . . . . . . 9 (𝜑 → (𝐵 supp 0) ∈ Fin)
280 ssidd 3967 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 supp 0) ⊆ (𝐵 supp 0))
281 c0ex 11149 . . . . . . . . . . . . . . . . 17 0 ∈ V
282281a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ V)
283208, 280, 23, 282suppssr 8127 . . . . . . . . . . . . . . 15 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐵𝑣) = 0)
284283oveq1d 7372 . . . . . . . . . . . . . 14 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐵𝑣) (𝑔𝑣)) = (0 (𝑔𝑣)))
285284adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) (𝑔𝑣)) = (0 (𝑔𝑣)))
286268adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → 𝑔:𝐼𝐾)
287 eldifi 4086 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝐼 ∖ (𝐵 supp 0)) → 𝑣𝐼)
288287ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → 𝑣𝐼)
289286, 288ffvelcdmd 7036 . . . . . . . . . . . . . 14 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → (𝑔𝑣) ∈ 𝐾)
290246, 71ringidval 19915 . . . . . . . . . . . . . . 15 (1r𝑆) = (0g𝑀)
291262, 290, 247mulg0 18879 . . . . . . . . . . . . . 14 ((𝑔𝑣) ∈ 𝐾 → (0 (𝑔𝑣)) = (1r𝑆))
292289, 291syl 17 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → (0 (𝑔𝑣)) = (1r𝑆))
293285, 292eqtrd 2776 . . . . . . . . . . . 12 (((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾m 𝐼)) → ((𝐵𝑣) (𝑔𝑣)) = (1r𝑆))
294293mpteq2dva 5205 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (1r𝑆)))
295 fconstmpt 5694 . . . . . . . . . . . 12 ((𝐾m 𝐼) × {(1r𝑆)}) = (𝑔 ∈ (𝐾m 𝐼) ↦ (1r𝑆))
296 ovexd 7392 . . . . . . . . . . . . 13 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐾m 𝐼) ∈ V)
29755, 296, 184syl2an2r 683 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐾m 𝐼) × {(1r𝑆)}) = (1r‘(𝑆s (𝐾m 𝐼))))
298295, 297eqtr3id 2790 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾m 𝐼) ↦ (1r𝑆)) = (1r‘(𝑆s (𝐾m 𝐼))))
299294, 298eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))) = (1r‘(𝑆s (𝐾m 𝐼))))
300299, 23suppss2 8131 . . . . . . . . 9 (𝜑 → ((𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) supp (1r‘(𝑆s (𝐾m 𝐼)))) ⊆ (𝐵 supp 0))
301279, 300ssfid 9211 . . . . . . . 8 (𝜑 → ((𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) supp (1r‘(𝑆s (𝐾m 𝐼)))) ∈ Fin)
302273, 274, 276, 301isfsuppd 40665 . . . . . . 7 (𝜑 → (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣)))) finSupp (1r‘(𝑆s (𝐾m 𝐼))))
30342, 41, 188, 43, 246, 56, 23, 49, 272, 302pwsgprod 40720 . . . . . 6 (𝜑 → ((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑣𝐼 ↦ (𝑔 ∈ (𝐾m 𝐼) ↦ ((𝐵𝑣) (𝑔𝑣))))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
304198, 261, 3033eqtrd 2780 . . . . 5 (𝜑 → ((1r‘(𝑆s (𝐾m 𝐼)))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝐵f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
305206, 187, 3043eqtrd 2780 . . . 4 (𝜑 → ((𝑆s (𝐾m 𝐼)) Σg (𝑏 ∈ {𝐵} ↦ (((𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))‘(𝐹𝑏))(.r‘(𝑆s (𝐾m 𝐼)))((mulGrp‘(𝑆s (𝐾m 𝐼))) Σg (𝑏f (.g‘(mulGrp‘(𝑆s (𝐾m 𝐼))))(𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))))))) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
30652, 168, 3053eqtrd 2780 . . 3 (𝜑 → (𝑄𝐹) = (𝑔 ∈ (𝐾m 𝐼) ↦ (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝑔𝑣))))))
307 evlsbagval.a . . 3 (𝜑𝐴 ∈ (𝐾m 𝐼))
308 ovexd 7392 . . 3 (𝜑 → (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))) ∈ V)
30934, 306, 307, 308fvmptd4 40658 . 2 (𝜑 → ((𝑄𝐹)‘𝐴) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣)))))
31030, 309jca 512 1 (𝜑 → (𝐹𝑊 ∧ ((𝑄𝐹)‘𝐴) = (𝑀 Σg (𝑣𝐼 ↦ ((𝐵𝑣) (𝐴𝑣))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wcel 2106  {crab 3407  Vcvv 3445  cdif 3907  wss 3910  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631  ccnv 5632  cres 5635  cima 5636  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  f cof 7615   supp csupp 8092  m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  0cc0 11051  cn 12153  0cn0 12413  Basecbs 17083  s cress 17112  .rcmulr 17134  0gc0g 17321   Σg cgsu 17322  s cpws 17328  Mndcmnd 18556  .gcmg 18872  CMndccmn 19562  mulGrpcmgp 19896  1rcur 19913  Ringcrg 19964  CRingccrg 19965  SubRingcsubrg 20218   mPwSer cmps 21306   mPoly cmpl 21308   evalSub ces 21480
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-srg 19918  df-ring 19966  df-cring 19967  df-rnghom 20146  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-assa 21259  df-asp 21260  df-ascl 21261  df-psr 21311  df-mvr 21312  df-mpl 21313  df-evls 21482
This theorem is referenced by:  mhphf  40757
  Copyright terms: Public domain W3C validator