evlsbagval - Mathbox for Steven Nguyen

	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 = (0_g‘𝑈)
evlsbagval.o	⊢ 1 = (1_r‘𝑈)
evlsbagval.d	⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ 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.

Step	Hyp	Ref	Expression
1		fvexd 6666	. . . . 5 ⊢ (𝜑 → (Base‘𝑈) ∈ V)
2		evlsbagval.d	. . . . . 6 ⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
3		ovexd 7178	. . . . . 6 ⊢ (𝜑 → (ℕ₀ ↑_m 𝐼) ∈ V)
4	2, 3	rabexd 5196	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ V)
5		evlsbagval.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
6		evlsbagval.u	. . . . . . . . . . 11 ⊢ 𝑈 = (𝑆 ↾_s 𝑅)
7	6	subrgring 19591	. . . . . . . . . 10 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
8	5, 7	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ Ring)
9		eqid 2759	. . . . . . . . . 10 ⊢ (Base‘𝑈) = (Base‘𝑈)
10		evlsbagval.o	. . . . . . . . . 10 ⊢ 1 = (1_r‘𝑈)
11	9, 10	ringidcl 19374	. . . . . . . . 9 ⊢ (𝑈 ∈ Ring → 1 ∈ (Base‘𝑈))
12	8, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (Base‘𝑈))
13		evlsbagval.z	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝑈)
14	9, 13	ring0cl 19375	. . . . . . . . 9 ⊢ (𝑈 ∈ Ring → 0 ∈ (Base‘𝑈))
15	8, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (Base‘𝑈))
16	12, 15	ifcld 4459	. . . . . . 7 ⊢ (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
17	16	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
18		evlsbagval.f	. . . . . 6 ⊢ 𝐹 = (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 ))
19	17, 18	fmptd 6862	. . . . 5 ⊢ (𝜑 → 𝐹:𝐷⟶(Base‘𝑈))
20	1, 4, 19	elmapdd 39707	. . . 4 ⊢ (𝜑 → 𝐹 ∈ ((Base‘𝑈) ↑_m 𝐷))
21		eqid 2759	. . . . 5 ⊢ (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
22		eqid 2759	. . . . 5 ⊢ (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
23		evlsbagval.i	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
24	21, 9, 2, 22, 23	psrbas 20691	. . . 4 ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑_m 𝐷))
25	20, 24	eleqtrrd 2854	. . 3 ⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)))
26	4, 15, 18	sniffsupp 8882	. . 3 ⊢ (𝜑 → 𝐹 finSupp 0 )
27		evlsbagval.p	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑈)
28		evlsbagval.w	. . . 4 ⊢ 𝑊 = (Base‘𝑃)
29	27, 21, 22, 13, 28	mplelbas 20743	. . 3 ⊢ (𝐹 ∈ 𝑊 ↔ (𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ 𝐹 finSupp 0 ))
30	25, 26, 29	sylanbrc 587	. 2 ⊢ (𝜑 → 𝐹 ∈ 𝑊)
31		fveq1 6650	. . . . . . . . 9 ⊢ (𝑝 = 𝐹 → (𝑝‘𝑏) = (𝐹‘𝑏))
32	31	fveq2d 6655	. . . . . . . 8 ⊢ (𝑝 = 𝐹 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝑝‘𝑏)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)))
33	32	oveq1d 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 𝐼) ↦ (𝑎‘𝑥)))))))
34	33	mpteq2dv 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 𝐼) ↦ (𝑎‘𝑥))))))))
35	34	oveq2d 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)
46	36, 27, 28, 2, 37, 6, 38, 39, 40, 41, 42, 43, 44, 23, 45, 5	evlsval3 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)
48	35, 46, 30, 47	fvmptd4 39701	. . . 4 ⊢ (𝜑 → (𝑄‘𝐹) = ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) Σ_g (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))))))
49	48	fveq1d 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 ⊢ (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
52	45	crngringd 19363	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Ring)
53		ovexd 7178	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ↑_m 𝐼) ∈ V)
54	38	pwsring 19421	. . . . . . . 8 ⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V) → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring)
55	52, 53, 54	syl2anc 588	. . . . . . 7 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring)
56	55	ringcmnd 39738	. . . . . 6 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CMnd)
57	55	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring)
58	45	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → 𝑆 ∈ CRing)
59		ovexd 7178	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → (𝐾 ↑_m 𝐼) ∈ V)
60	37	subrgss 19589	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾)
61	5, 60	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ⊆ 𝐾)
62	61	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑅 ⊆ 𝐾)
63	62	sselda 3888	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝐾)
64		fconst6g 6546	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐾 → ((𝐾 ↑_m 𝐼) × {𝑥}):(𝐾 ↑_m 𝐼)⟶𝐾)
65	63, 64	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → ((𝐾 ↑_m 𝐼) × {𝑥}):(𝐾 ↑_m 𝐼)⟶𝐾)
66	38, 37, 50, 58, 59, 65	pwselbasr 39758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → ((𝐾 ↑_m 𝐼) × {𝑥}) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
67	66	fmpttd 6863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥})):𝑅⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
68		eqid 2759	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘𝑆) = (1_r‘𝑆)
69	6, 68	subrg1 19598	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (1_r‘𝑆) = (1_r‘𝑈))
70	5, 69	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝑆) = (1_r‘𝑈))
71	68	subrg1cl 19596	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (1_r‘𝑆) ∈ 𝑅)
72	5, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝑆) ∈ 𝑅)
73	70, 72	eqeltrrd 2852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1_r‘𝑈) ∈ 𝑅)
74	10, 73	eqeltrid 2855	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ 𝑅)
75	6	subrgbas 19597	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
76	5, 75	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 = (Base‘𝑈))
77	15, 76	eleqtrrd 2854	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ 𝑅)
78	74, 77	ifcld 4459	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
79	78	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
80	79, 18	fmptd 6862	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐷⟶𝑅)
81	80	ffvelrnda 6835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘𝑏) ∈ 𝑅)
82	67, 81	ffvelrnd 6836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
83	39, 50	mgpbas 19298	. . . . . . . . 9 ⊢ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (Base‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
84	38	pwscrng 19423	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ CRing ∧ (𝐾 ↑_m 𝐼) ∈ V) → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CRing)
85	45, 53, 84	syl2anc 588	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CRing)
86	39	crngmgp 19358	. . . . . . . . . . 11 ⊢ ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CRing → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
88	87	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
89		simpr 489	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
90	45	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
91		ovexd 7178	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
92		elmapi 8431	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) → 𝑎:𝐼⟶𝐾)
93	92	adantl 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
94		simplr 769	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑥 ∈ 𝐼)
95	93, 94	ffvelrnd 6836	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑥) ∈ 𝐾)
96	95	fmpttd 6863	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)):(𝐾 ↑_m 𝐼)⟶𝐾)
97	38, 37, 50, 90, 91, 96	pwselbasr 39758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
98	97	fmpttd 6863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))):𝐼⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
99	2, 83, 40, 88, 89, 98	psrbagev2 20825	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
100	50, 41, 57, 82, 99	ringcld 39733	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
101	100	fmpttd 6863	. . . . . 6 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))):𝐷⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
102		eqeq1 2763	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑏 → (𝑠 = 𝐵 ↔ 𝑏 = 𝐵))
103	102	ifbid 4436	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑏 → if(𝑠 = 𝐵, 1 , 0 ) = if(𝑏 = 𝐵, 1 , 0 ))
104		eldifi 4028	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐵}) → 𝑏 ∈ 𝐷)
105	104	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → 𝑏 ∈ 𝐷)
106	10	fvexi 6665	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
107	13	fvexi 6665	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
108	106, 107	ifex 4463	. . . . . . . . . . . . . 14 ⊢ if(𝑏 = 𝐵, 1 , 0 ) ∈ V
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) ∈ V)
110	18, 103, 105, 109	fvmptd3 6775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹‘𝑏) = if(𝑏 = 𝐵, 1 , 0 ))
111		eldifsnneq 4674	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐵}) → ¬ 𝑏 = 𝐵)
112	111	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ¬ 𝑏 = 𝐵)
113	112	iffalsed 4424	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) = 0 )
114	110, 113	eqtrd 2794	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹‘𝑏) = 0 )
115	114	fveq2d 6655	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 0 ))
116		sneq 4525	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → {𝑥} = { 0 })
117	116	xpeq2d 5547	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → ((𝐾 ↑_m 𝐼) × {𝑥}) = ((𝐾 ↑_m 𝐼) × { 0 }))
118	77	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → 0 ∈ 𝑅)
119		ovex 7176	. . . . . . . . . . . . 13 ⊢ (𝐾 ↑_m 𝐼) ∈ V
120		snex 5293	. . . . . . . . . . . . 13 ⊢ { 0 } ∈ V
121	119, 120	xpex 7467	. . . . . . . . . . . 12 ⊢ ((𝐾 ↑_m 𝐼) × { 0 }) ∈ V
122	121	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾 ↑_m 𝐼) × { 0 }) ∈ V)
123	43, 117, 118, 122	fvmptd3 6775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 0 ) = ((𝐾 ↑_m 𝐼) × { 0 }))
124		eqid 2759	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
125	6, 124	subrg0 19595	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (0_g‘𝑆) = (0_g‘𝑈))
126	5, 125	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝑆) = (0_g‘𝑈))
127	126, 13	eqtr4di 2812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑆) = 0 )
128	127	sneqd 4527	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(0_g‘𝑆)} = { 0 })
129	128	xpeq2d 5547	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(0_g‘𝑆)}) = ((𝐾 ↑_m 𝐼) × { 0 }))
130	52	ringgrpd 19359	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ Grp)
131	130	grpmndd 18166	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Mnd)
132	38, 124	pws0g 17998	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Mnd ∧ (𝐾 ↑_m 𝐼) ∈ V) → ((𝐾 ↑_m 𝐼) × {(0_g‘𝑆)}) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
133	131, 53, 132	syl2anc 588	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(0_g‘𝑆)}) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
134	129, 133	eqtr3d 2796	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × { 0 }) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
135	134	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾 ↑_m 𝐼) × { 0 }) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
136	115, 123, 135	3eqtrd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
137	136	oveq1d 7158	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = ((0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))))
138	87	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
139	45	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
140		ovexd 7178	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
141	92	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
142		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑥 ∈ 𝐼)
143	141, 142	ffvelrnd 6836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑥) ∈ 𝐾)
144	143	fmpttd 6863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)):(𝐾 ↑_m 𝐼)⟶𝐾)
145	38, 37, 50, 139, 140, 144	pwselbasr 39758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
146	145	fmpttd 6863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))):𝐼⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
147	2, 83, 40, 138, 105, 146	psrbagev2 20825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
148	50, 41, 51	ringlz 19393	. . . . . . . . 9 ⊢ (((𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring ∧ ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) → ((0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
149	55, 147, 148	syl2an2r 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
150	137, 149	eqtrd 2794	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
151	150, 4	suppss2 7867	. . . . . 6 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))) supp (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ⊆ {𝐵})
152	4	mptexd 6971	. . . . . . 7 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))) ∈ V)
153		fvexd 6666	. . . . . . 7 ⊢ (𝜑 → (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ V)
154		funmpt 6366	. . . . . . . 8 ⊢ Fun (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))))
155	154	a1i 11	. . . . . . 7 ⊢ (𝜑 → Fun (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))))
156		snfi 8607	. . . . . . . . 9 ⊢ {𝐵} ∈ Fin
157	156	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐵} ∈ Fin)
158	157, 151	ssfid 8755	. . . . . . 7 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))) supp (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ∈ Fin)
159	152, 153, 155, 158	isfsuppd 39708	. . . . . 6 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))) finSupp (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
160	50, 51, 56, 4, 101, 151, 159	gsumres 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 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
162	161	snssd 4692	. . . . . . 7 ⊢ (𝜑 → {𝐵} ⊆ 𝐷)
163	162	resmptd 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 𝐼) ↦ (𝑎‘𝑥))))))))
164	163	oveq2d 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 𝐼) ↦ (𝑎‘𝑥)))))))))
165	160, 164	eqtr3d 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 𝐼) ↦ (𝑎‘𝑥)))))))))
166	165	fveq1d 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 ⊢ (𝑔 = 𝐴 → (𝑔‘𝑣) = (𝐴‘𝑣))
168	167	oveq2d 7159	. . . . . 6 ⊢ (𝑔 = 𝐴 → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))
169	168	mpteq2dv 5121	. . . . 5 ⊢ (𝑔 = 𝐴 → (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣))))
170	169	oveq2d 7159	. . . 4 ⊢ (𝑔 = 𝐴 → (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))
171	55	ringgrpd 19359	. . . . . . 7 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Grp)
172	171	grpmndd 18166	. . . . . 6 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Mnd)
173		iftrue 4419	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝐵 → if(𝑠 = 𝐵, 1 , 0 ) = 1 )
174	106	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
175	18, 173, 161, 174	fvmptd3 6775	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝐵) = 1 )
176	175	fveq2d 6655	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 1 ))
177	10, 70	eqtr4id 2813	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (1_r‘𝑆))
178	177	fveq2d 6655	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 1 ) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(1_r‘𝑆)))
179		sneq 4525	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1_r‘𝑆) → {𝑥} = {(1_r‘𝑆)})
180	179	xpeq2d 5547	. . . . . . . . . . . 12 ⊢ (𝑥 = (1_r‘𝑆) → ((𝐾 ↑_m 𝐼) × {𝑥}) = ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}))
181		snex 5293	. . . . . . . . . . . . . 14 ⊢ {(1_r‘𝑆)} ∈ V
182	181	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(1_r‘𝑆)} ∈ V)
183	53, 182	xpexd 7465	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) ∈ V)
184	43, 180, 72, 183	fvmptd3 6775	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(1_r‘𝑆)) = ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}))
185	178, 184	eqtrd 2794	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 1 ) = ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}))
186	38, 68	pws1 19422	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V) → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
187	52, 53, 186	syl2anc 588	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
188	176, 185, 187	3eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵)) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
189	188	oveq1d 7158	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = ((1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))))
190	45	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
191		ovexd 7178	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
192	92	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
193		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑥 ∈ 𝐼)
194	192, 193	ffvelrnd 6836	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑥) ∈ 𝐾)
195	194	fmpttd 6863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)):(𝐾 ↑_m 𝐼)⟶𝐾)
196	38, 37, 50, 190, 191, 195	pwselbasr 39758	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
197	196	fmpttd 6863	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))):𝐼⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
198	2, 83, 40, 87, 161, 197	psrbagev2 20825	. . . . . . . . 9 ⊢ (𝜑 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
199		eqid 2759	. . . . . . . . . 10 ⊢ (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
200	50, 41, 199	ringlidm 19377	. . . . . . . . 9 ⊢ (((𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring ∧ ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) → ((1_r‘(𝑆 ↑_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 𝐼) ↦ (𝑎‘𝑥))))))
201	55, 198, 200	syl2anc 588	. . . . . . . 8 ⊢ (𝜑 → ((1_r‘(𝑆 ↑_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 𝐼) ↦ (𝑎‘𝑥))))))
202	189, 201	eqtrd 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 𝐼) ↦ (𝑎‘𝑥))))))
203	202, 198	eqeltrd 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 𝐼) ↦ (𝑎‘𝑥)))))
206	205	oveq2d 7159	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) = ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))
207	204, 206	oveq12d 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 𝐼) ↦ (𝑎‘𝑥)))))))
208	50, 207	gsumsn 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 𝐼) ↦ (𝑎‘𝑥)))))))
209	172, 161, 203, 208	syl3anc 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 𝐼) ↦ (𝑎‘𝑥)))))))
210	2	psrbagf 20665	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐷 → 𝐵:𝐼⟶ℕ₀)
211	161, 210	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵:𝐼⟶ℕ₀)
212	211	ffnd 6492	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 Fn 𝐼)
213	119	mptex 6970	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ V
214	213, 44	fnmpti 6467	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼
215	214	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼)
216		inidm 4119	. . . . . . . . 9 ⊢ (𝐼 ∩ 𝐼) = 𝐼
217		eqidd 2760	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐵‘𝑣) = (𝐵‘𝑣))
218		fveq2 6651	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑣 → (𝑎‘𝑥) = (𝑎‘𝑣))
219	218	mpteq2dv 5121	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) = (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))
220		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
221	119	mptex 6970	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ V
222	221	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ V)
223	44, 219, 220, 222	fvmptd3 6775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))‘𝑣) = (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))
224	212, 215, 23, 23, 216, 217, 223	offval 7406	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))))
225	45	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → 𝑆 ∈ CRing)
226		ovexd 7178	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
227	39	ringmgp 19356	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd)
228	55, 227	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd)
229	228	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd)
230	211	ffvelrnda 6835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐵‘𝑣) ∈ ℕ₀)
231	92	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
232		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑣 ∈ 𝐼)
233	231, 232	ffvelrnd 6836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑣) ∈ 𝐾)
234	233	fmpttd 6863	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)):(𝐾 ↑_m 𝐼)⟶𝐾)
235	38, 37, 50, 225, 226, 234	pwselbasr 39758	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
236	83, 40	mulgnn0cl 18296	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd ∧ (𝐵‘𝑣) ∈ ℕ₀ ∧ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
237	229, 230, 235, 236	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
238	38, 37, 50, 225, 226, 237	pwselbas 16805	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))):(𝐾 ↑_m 𝐼)⟶𝐾)
239	238	ffnd 6492	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) Fn (𝐾 ↑_m 𝐼))
240		ovex 7176	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) ∈ V
241		eqid 2759	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))
242	240, 241	fnmpti 6467	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) Fn (𝐾 ↑_m 𝐼)
243	242	a1i 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)
248	244, 245, 246, 247	fvmptd3 6775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))‘𝑙) = (𝑙‘𝑣))
249	248	oveq2d 7159	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ ((𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))‘𝑙)) = ((𝐵‘𝑣) ↑ (𝑙‘𝑣)))
250		evlsbagval.m	. . . . . . . . . . . 12 ⊢ 𝑀 = (mulGrp‘𝑆)
251		evlsbagval.e	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘𝑀)
252	52	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → 𝑆 ∈ Ring)
253		ovexd 7178	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝐾 ↑_m 𝐼) ∈ V)
254	230	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝐵‘𝑣) ∈ ℕ₀)
255	235	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
256	38, 50, 39, 250, 40, 251, 252, 253, 254, 255, 246	pwsexpg 39760	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))‘𝑙) = ((𝐵‘𝑣) ↑ ((𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))‘𝑙)))
257		fveq1 6650	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑙 → (𝑔‘𝑣) = (𝑙‘𝑣))
258	257	oveq2d 7159	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑙 → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = ((𝐵‘𝑣) ↑ (𝑙‘𝑣)))
259		ovexd 7178	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ (𝑙‘𝑣)) ∈ V)
260	241, 258, 246, 259	fvmptd3 6775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))‘𝑙) = ((𝐵‘𝑣) ↑ (𝑙‘𝑣)))
261	249, 256, 260	3eqtr4d 2804	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))‘𝑙) = ((𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))‘𝑙))
262	239, 243, 261	eqfnfvd 6789	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))
263	262	mpteq2dva 5120	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))) = (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))))
264	224, 263	eqtrd 2794	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))))
265	264	oveq2d 7159	. . . . . 6 ⊢ (𝜑 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) = ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))))
266	250	crngmgp 19358	. . . . . . . . . . 11 ⊢ (𝑆 ∈ CRing → 𝑀 ∈ CMnd)
267	45, 266	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ CMnd)
268	267	cmnmndd 18981	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ Mnd)
269	268	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → 𝑀 ∈ Mnd)
270	230	adantrl 716	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → (𝐵‘𝑣) ∈ ℕ₀)
271		elmapi 8431	. . . . . . . . . 10 ⊢ (𝑔 ∈ (𝐾 ↑_m 𝐼) → 𝑔:𝐼⟶𝐾)
272	271	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → 𝑔:𝐼⟶𝐾)
273		simprr 773	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → 𝑣 ∈ 𝐼)
274	272, 273	ffvelrnd 6836	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → (𝑔‘𝑣) ∈ 𝐾)
275	250, 37	mgpbas 19298	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑀)
276	275, 251	mulgnn0cl 18296	. . . . . . . 8 ⊢ ((𝑀 ∈ Mnd ∧ (𝐵‘𝑣) ∈ ℕ₀ ∧ (𝑔‘𝑣) ∈ 𝐾) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) ∈ 𝐾)
277	269, 270, 274, 276	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) ∈ 𝐾)
278	23	mptexd 6971	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) ∈ V)
279		fvexd 6666	. . . . . . . 8 ⊢ (𝜑 → (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ V)
280		funmpt 6366	. . . . . . . . 9 ⊢ Fun (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))
281	280	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Fun (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))))
282	2	psrbagfsupp 20667	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐷 → 𝐵 finSupp 0)
283	161, 282	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 finSupp 0)
284	283	fsuppimpd 8858	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 supp 0) ∈ Fin)
285		ssidd 3911	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 supp 0) ⊆ (𝐵 supp 0))
286		c0ex 10658	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
287	286	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ V)
288	211, 285, 23, 287	suppssr 7863	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐵‘𝑣) = 0)
289	288	oveq1d 7158	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = (0 ↑ (𝑔‘𝑣)))
290	289	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = (0 ↑ (𝑔‘𝑣)))
291	271	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → 𝑔:𝐼⟶𝐾)
292		eldifi 4028	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝐼 ∖ (𝐵 supp 0)) → 𝑣 ∈ 𝐼)
293	292	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → 𝑣 ∈ 𝐼)
294	291, 293	ffvelrnd 6836	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → (𝑔‘𝑣) ∈ 𝐾)
295	250, 68	ringidval 19306	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑆) = (0_g‘𝑀)
296	275, 295, 251	mulg0 18283	. . . . . . . . . . . . . 14 ⊢ ((𝑔‘𝑣) ∈ 𝐾 → (0 ↑ (𝑔‘𝑣)) = (1_r‘𝑆))
297	294, 296	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → (0 ↑ (𝑔‘𝑣)) = (1_r‘𝑆))
298	290, 297	eqtrd 2794	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = (1_r‘𝑆))
299	298	mpteq2dva 5120	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (1_r‘𝑆)))
300		fconstmpt 5576	. . . . . . . . . . . 12 ⊢ ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (1_r‘𝑆))
301		ovexd 7178	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐾 ↑_m 𝐼) ∈ V)
302	52, 301, 186	syl2an2r 685	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
303	300, 302	syl5eqr 2808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (1_r‘𝑆)) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
304	299, 303	eqtrd 2794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
305	304, 23	suppss2 7867	. . . . . . . . 9 ⊢ (𝜑 → ((𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) supp (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ⊆ (𝐵 supp 0))
306	284, 305	ssfid 8755	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) supp (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ∈ Fin)
307	278, 279, 281, 306	isfsuppd 39708	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) finSupp (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
308	38, 37, 199, 39, 250, 53, 23, 45, 277, 307	pwsgprod 39761	. . . . . 6 ⊢ (𝜑 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))))
309	201, 265, 308	3eqtrd 2798	. . . . 5 ⊢ (𝜑 → ((1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))))
310	209, 189, 309	3eqtrd 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)
313	170, 310, 311, 312	fvmptd4 39701	. . 3 ⊢ (𝜑 → (((𝑆 ↑_s (𝐾 ↑_m 𝐼)) Σ_g (𝑏 ∈ {𝐵} ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))))‘𝐴) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))
314	49, 166, 313	3eqtrd 2798	. 2 ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))
315	30, 314	jca 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 ℕ₀cn0 11919 Basecbs 16526 ↾_s cress 16527 ._rcmulr 16609 0_gc0g 16756 Σ_g cgsu 16757 ↑_s cpws 16763 Mndcmnd 17962 ._gcmg 18276 CMndccmn 18958 mulGrpcmgp 19292 1_rcur 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

W3C validator