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 39808

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 39818, 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 6677	. . . . 5 ⊢ (𝜑 → (Base‘𝑈) ∈ V)
2		evlsbagval.d	. . . . . 6 ⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
3		ovexd 7190	. . . . . 6 ⊢ (𝜑 → (ℕ₀ ↑_m 𝐼) ∈ V)
4	2, 3	rabexd 5206	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ V)
5		evlsbagval.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
6		evlsbagval.u	. . . . . . . . . . 11 ⊢ 𝑈 = (𝑆 ↾_s 𝑅)
7	6	subrgring 19611	. . . . . . . . . 10 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
8	5, 7	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ Ring)
9		eqid 2758	. . . . . . . . . 10 ⊢ (Base‘𝑈) = (Base‘𝑈)
10		evlsbagval.o	. . . . . . . . . 10 ⊢ 1 = (1_r‘𝑈)
11	9, 10	ringidcl 19394	. . . . . . . . 9 ⊢ (𝑈 ∈ Ring → 1 ∈ (Base‘𝑈))
12	8, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (Base‘𝑈))
13		evlsbagval.z	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝑈)
14	9, 13	ring0cl 19395	. . . . . . . . 9 ⊢ (𝑈 ∈ Ring → 0 ∈ (Base‘𝑈))
15	8, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (Base‘𝑈))
16	12, 15	ifcld 4469	. . . . . . 7 ⊢ (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
17	16	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ (Base‘𝑈))
18		evlsbagval.f	. . . . . 6 ⊢ 𝐹 = (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 ))
19	17, 18	fmptd 6874	. . . . 5 ⊢ (𝜑 → 𝐹:𝐷⟶(Base‘𝑈))
20	1, 4, 19	elmapdd 39751	. . . 4 ⊢ (𝜑 → 𝐹 ∈ ((Base‘𝑈) ↑_m 𝐷))
21		eqid 2758	. . . . 5 ⊢ (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
22		eqid 2758	. . . . 5 ⊢ (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
23		evlsbagval.i	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
24	21, 9, 2, 22, 23	psrbas 20711	. . . 4 ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑_m 𝐷))
25	20, 24	eleqtrrd 2855	. . 3 ⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)))
26	4, 15, 18	sniffsupp 8902	. . 3 ⊢ (𝜑 → 𝐹 finSupp 0 )
27		evlsbagval.p	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑈)
28		evlsbagval.w	. . . 4 ⊢ 𝑊 = (Base‘𝑃)
29	27, 21, 22, 13, 28	mplelbas 20763	. . 3 ⊢ (𝐹 ∈ 𝑊 ↔ (𝐹 ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ 𝐹 finSupp 0 ))
30	25, 26, 29	sylanbrc 586	. 2 ⊢ (𝜑 → 𝐹 ∈ 𝑊)
31		fveq1 6661	. . . . . . . . 9 ⊢ (𝑝 = 𝐹 → (𝑝‘𝑏) = (𝐹‘𝑏))
32	31	fveq2d 6666	. . . . . . . 8 ⊢ (𝑝 = 𝐹 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝑝‘𝑏)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)))
33	32	oveq1d 7170	. . . . . . 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 5131	. . . . . 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 7171	. . . . 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 2758	. . . . . 6 ⊢ (𝑆 ↑_s (𝐾 ↑_m 𝐼)) = (𝑆 ↑_s (𝐾 ↑_m 𝐼))
39		eqid 2758	. . . . . 6 ⊢ (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
40		eqid 2758	. . . . . 6 ⊢ (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) = (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
41		eqid 2758	. . . . . 6 ⊢ (._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
42		eqid 2758	. . . . . 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 2758	. . . . . 6 ⊢ (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))
44		eqid 2758	. . . . . 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 39805	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑝 ∈ 𝑊 ↦ ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) Σ_g (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝑝‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))))))
47		ovexd 7190	. . . . 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 39745	. . . 4 ⊢ (𝜑 → (𝑄‘𝐹) = ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) Σ_g (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))))))
49	48	fveq1d 6664	. . 3 ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (((𝑆 ↑_s (𝐾 ↑_m 𝐼)) Σ_g (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))))‘𝐴))
50		eqid 2758	. . . . . 6 ⊢ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
51		eqid 2758	. . . . . 6 ⊢ (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
52	45	crngringd 19383	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Ring)
53		ovexd 7190	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ↑_m 𝐼) ∈ V)
54	38	pwsring 19441	. . . . . . . 8 ⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V) → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring)
55	52, 53, 54	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring)
56	55	ringcmnd 39781	. . . . . 6 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CMnd)
57	55	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring)
58	45	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → 𝑆 ∈ CRing)
59		ovexd 7190	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → (𝐾 ↑_m 𝐼) ∈ V)
60	37	subrgss 19609	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾)
61	5, 60	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ⊆ 𝐾)
62	61	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑅 ⊆ 𝐾)
63	62	sselda 3894	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝐾)
64		fconst6g 6557	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐾 → ((𝐾 ↑_m 𝐼) × {𝑥}):(𝐾 ↑_m 𝐼)⟶𝐾)
65	63, 64	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → ((𝐾 ↑_m 𝐼) × {𝑥}):(𝐾 ↑_m 𝐼)⟶𝐾)
66	38, 37, 50, 58, 59, 65	pwselbasr 39801	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝑅) → ((𝐾 ↑_m 𝐼) × {𝑥}) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
67	66	fmpttd 6875	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥})):𝑅⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
68		eqid 2758	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘𝑆) = (1_r‘𝑆)
69	6, 68	subrg1 19618	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (1_r‘𝑆) = (1_r‘𝑈))
70	5, 69	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝑆) = (1_r‘𝑈))
71	68	subrg1cl 19616	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (1_r‘𝑆) ∈ 𝑅)
72	5, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝑆) ∈ 𝑅)
73	70, 72	eqeltrrd 2853	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1_r‘𝑈) ∈ 𝑅)
74	10, 73	eqeltrid 2856	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ 𝑅)
75	6	subrgbas 19617	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
76	5, 75	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 = (Base‘𝑈))
77	15, 76	eleqtrrd 2855	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ 𝑅)
78	74, 77	ifcld 4469	. . . . . . . . . . . 12 ⊢ (𝜑 → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
79	78	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → if(𝑠 = 𝐵, 1 , 0 ) ∈ 𝑅)
80	79, 18	fmptd 6874	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐷⟶𝑅)
81	80	ffvelrnda 6847	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘𝑏) ∈ 𝑅)
82	67, 81	ffvelrnd 6848	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
83	39, 50	mgpbas 19318	. . . . . . . . 9 ⊢ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (Base‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
84	38	pwscrng 19443	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ CRing ∧ (𝐾 ↑_m 𝐼) ∈ V) → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CRing)
85	45, 53, 84	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CRing)
86	39	crngmgp 19378	. . . . . . . . . . 11 ⊢ ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ CRing → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
88	87	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
89		simpr 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
90	45	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
91		ovexd 7190	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
92		elmapi 8443	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) → 𝑎:𝐼⟶𝐾)
93	92	adantl 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
94		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑥 ∈ 𝐼)
95	93, 94	ffvelrnd 6848	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑥) ∈ 𝐾)
96	95	fmpttd 6875	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)):(𝐾 ↑_m 𝐼)⟶𝐾)
97	38, 37, 50, 90, 91, 96	pwselbasr 39801	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
98	97	fmpttd 6875	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))):𝐼⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
99	2, 83, 40, 88, 89, 98	psrbagev2 20845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
100	50, 41, 57, 82, 99	ringcld 39776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
101	100	fmpttd 6875	. . . . . 6 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))):𝐷⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
102		eqeq1 2762	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑏 → (𝑠 = 𝐵 ↔ 𝑏 = 𝐵))
103	102	ifbid 4446	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑏 → if(𝑠 = 𝐵, 1 , 0 ) = if(𝑏 = 𝐵, 1 , 0 ))
104		eldifi 4034	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐵}) → 𝑏 ∈ 𝐷)
105	104	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → 𝑏 ∈ 𝐷)
106	10	fvexi 6676	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
107	13	fvexi 6676	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
108	106, 107	ifex 4473	. . . . . . . . . . . . . 14 ⊢ if(𝑏 = 𝐵, 1 , 0 ) ∈ V
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) ∈ V)
110	18, 103, 105, 109	fvmptd3 6786	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹‘𝑏) = if(𝑏 = 𝐵, 1 , 0 ))
111		eldifsnneq 4684	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐵}) → ¬ 𝑏 = 𝐵)
112	111	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ¬ 𝑏 = 𝐵)
113	112	iffalsed 4434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → if(𝑏 = 𝐵, 1 , 0 ) = 0 )
114	110, 113	eqtrd 2793	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝐹‘𝑏) = 0 )
115	114	fveq2d 6666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 0 ))
116		sneq 4535	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → {𝑥} = { 0 })
117	116	xpeq2d 5557	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → ((𝐾 ↑_m 𝐼) × {𝑥}) = ((𝐾 ↑_m 𝐼) × { 0 }))
118	77	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → 0 ∈ 𝑅)
119		ovex 7188	. . . . . . . . . . . . 13 ⊢ (𝐾 ↑_m 𝐼) ∈ V
120		snex 5303	. . . . . . . . . . . . 13 ⊢ { 0 } ∈ V
121	119, 120	xpex 7479	. . . . . . . . . . . 12 ⊢ ((𝐾 ↑_m 𝐼) × { 0 }) ∈ V
122	121	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾 ↑_m 𝐼) × { 0 }) ∈ V)
123	43, 117, 118, 122	fvmptd3 6786	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 0 ) = ((𝐾 ↑_m 𝐼) × { 0 }))
124		eqid 2758	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
125	6, 124	subrg0 19615	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (0_g‘𝑆) = (0_g‘𝑈))
126	5, 125	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝑆) = (0_g‘𝑈))
127	126, 13	eqtr4di 2811	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝑆) = 0 )
128	127	sneqd 4537	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(0_g‘𝑆)} = { 0 })
129	128	xpeq2d 5557	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(0_g‘𝑆)}) = ((𝐾 ↑_m 𝐼) × { 0 }))
130	52	ringgrpd 19379	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ Grp)
131	130	grpmndd 18186	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Mnd)
132	38, 124	pws0g 18018	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Mnd ∧ (𝐾 ↑_m 𝐼) ∈ V) → ((𝐾 ↑_m 𝐼) × {(0_g‘𝑆)}) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
133	131, 53, 132	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(0_g‘𝑆)}) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
134	129, 133	eqtr3d 2795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × { 0 }) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
135	134	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝐾 ↑_m 𝐼) × { 0 }) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
136	115, 123, 135	3eqtrd 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
137	136	oveq1d 7170	. . . . . . . 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 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ CMnd)
139	45	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
140		ovexd 7190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
141	92	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
142		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑥 ∈ 𝐼)
143	141, 142	ffvelrnd 6848	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑥) ∈ 𝐾)
144	143	fmpttd 6875	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)):(𝐾 ↑_m 𝐼)⟶𝐾)
145	38, 37, 50, 139, 140, 144	pwselbasr 39801	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
146	145	fmpttd 6875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))):𝐼⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
147	2, 83, 40, 138, 105, 146	psrbagev2 20845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
148	50, 41, 51	ringlz 19413	. . . . . . . . 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 684	. . . . . . . 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 2793	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐵})) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) = (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
151	150, 4	suppss2 7879	. . . . . 6 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))) supp (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ⊆ {𝐵})
152	4	mptexd 6983	. . . . . . 7 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))) ∈ V)
153		fvexd 6677	. . . . . . 7 ⊢ (𝜑 → (0_g‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ V)
154		funmpt 6377	. . . . . . . 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 8619	. . . . . . . . 9 ⊢ {𝐵} ∈ Fin
157	156	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐵} ∈ Fin)
158	157, 151	ssfid 8783	. . . . . . 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 39752	. . . . . 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 19106	. . . . 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 4702	. . . . . . 7 ⊢ (𝜑 → {𝐵} ⊆ 𝐷)
163	162	resmptd 5884	. . . . . 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 7171	. . . . 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 2795	. . . 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 6664	. . 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 6661	. . . . . . 7 ⊢ (𝑔 = 𝐴 → (𝑔‘𝑣) = (𝐴‘𝑣))
168	167	oveq2d 7171	. . . . . 6 ⊢ (𝑔 = 𝐴 → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))
169	168	mpteq2dv 5131	. . . . 5 ⊢ (𝑔 = 𝐴 → (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣))))
170	169	oveq2d 7171	. . . 4 ⊢ (𝑔 = 𝐴 → (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))
171	55	ringgrpd 19379	. . . . . . 7 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Grp)
172	171	grpmndd 18186	. . . . . 6 ⊢ (𝜑 → (𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Mnd)
173		iftrue 4429	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝐵 → if(𝑠 = 𝐵, 1 , 0 ) = 1 )
174	106	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
175	18, 173, 161, 174	fvmptd3 6786	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝐵) = 1 )
176	175	fveq2d 6666	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 1 ))
177	10, 70	eqtr4id 2812	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (1_r‘𝑆))
178	177	fveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 1 ) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(1_r‘𝑆)))
179		sneq 4535	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1_r‘𝑆) → {𝑥} = {(1_r‘𝑆)})
180	179	xpeq2d 5557	. . . . . . . . . . . 12 ⊢ (𝑥 = (1_r‘𝑆) → ((𝐾 ↑_m 𝐼) × {𝑥}) = ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}))
181		snex 5303	. . . . . . . . . . . . . 14 ⊢ {(1_r‘𝑆)} ∈ V
182	181	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(1_r‘𝑆)} ∈ V)
183	53, 182	xpexd 7477	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) ∈ V)
184	43, 180, 72, 183	fvmptd3 6786	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(1_r‘𝑆)) = ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}))
185	178, 184	eqtrd 2793	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘ 1 ) = ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}))
186	38, 68	pws1 19442	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V) → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
187	52, 53, 186	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
188	176, 185, 187	3eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵)) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
189	188	oveq1d 7170	. . . . . . . 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 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
191		ovexd 7190	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
192	92	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
193		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑥 ∈ 𝐼)
194	192, 193	ffvelrnd 6848	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑥) ∈ 𝐾)
195	194	fmpttd 6875	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)):(𝐾 ↑_m 𝐼)⟶𝐾)
196	38, 37, 50, 190, 191, 195	pwselbasr 39801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
197	196	fmpttd 6875	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))):𝐼⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
198	2, 83, 40, 87, 161, 197	psrbagev2 20845	. . . . . . . . 9 ⊢ (𝜑 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
199		eqid 2758	. . . . . . . . . 10 ⊢ (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
200	50, 41, 199	ringlidm 19397	. . . . . . . . 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 587	. . . . . . . 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 2793	. . . . . . 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 2852	. . . . . 6 ⊢ (𝜑 → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
204		2fveq3 6667	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝐵)))
205		oveq1 7162	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))) = (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))))
206	205	oveq2d 7171	. . . . . . . 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 7173	. . . . . . 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 19147	. . . . . 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 1368	. . . . 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 20685	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐷 → 𝐵:𝐼⟶ℕ₀)
211	161, 210	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵:𝐼⟶ℕ₀)
212	211	ffnd 6503	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 Fn 𝐼)
213	119	mptex 6982	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) ∈ V
214	213, 44	fnmpti 6478	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼
215	214	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼)
216		inidm 4125	. . . . . . . . 9 ⊢ (𝐼 ∩ 𝐼) = 𝐼
217		eqidd 2759	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐵‘𝑣) = (𝐵‘𝑣))
218		fveq2 6662	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑣 → (𝑎‘𝑥) = (𝑎‘𝑣))
219	218	mpteq2dv 5131	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)) = (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))
220		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
221	119	mptex 6982	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ V
222	221	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ V)
223	44, 219, 220, 222	fvmptd3 6786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))‘𝑣) = (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))
224	212, 215, 23, 23, 216, 217, 223	offval 7418	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))))
225	45	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → 𝑆 ∈ CRing)
226		ovexd 7190	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐾 ↑_m 𝐼) ∈ V)
227	39	ringmgp 19376	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ↑_s (𝐾 ↑_m 𝐼)) ∈ Ring → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd)
228	55, 227	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd)
229	228	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd)
230	211	ffvelrnda 6847	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐵‘𝑣) ∈ ℕ₀)
231	92	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑎:𝐼⟶𝐾)
232		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → 𝑣 ∈ 𝐼)
233	231, 232	ffvelrnd 6848	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑_m 𝐼)) → (𝑎‘𝑣) ∈ 𝐾)
234	233	fmpttd 6875	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)):(𝐾 ↑_m 𝐼)⟶𝐾)
235	38, 37, 50, 225, 226, 234	pwselbasr 39801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
236	83, 40	mulgnn0cl 18316	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ Mnd ∧ (𝐵‘𝑣) ∈ ℕ₀ ∧ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
237	229, 230, 235, 236	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
238	38, 37, 50, 225, 226, 237	pwselbas 16825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))):(𝐾 ↑_m 𝐼)⟶𝐾)
239	238	ffnd 6503	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) Fn (𝐾 ↑_m 𝐼))
240		ovex 7188	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) ∈ V
241		eqid 2758	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))
242	240, 241	fnmpti 6478	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) Fn (𝐾 ↑_m 𝐼)
243	242	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) Fn (𝐾 ↑_m 𝐼))
244		eqid 2758	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) = (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))
245		fveq1 6661	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑙 → (𝑎‘𝑣) = (𝑙‘𝑣))
246		simpr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → 𝑙 ∈ (𝐾 ↑_m 𝐼))
247		fvexd 6677	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝑙‘𝑣) ∈ V)
248	244, 245, 246, 247	fvmptd3 6786	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))‘𝑙) = (𝑙‘𝑣))
249	248	oveq2d 7171	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ ((𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))‘𝑙)) = ((𝐵‘𝑣) ↑ (𝑙‘𝑣)))
250		evlsbagval.m	. . . . . . . . . . . 12 ⊢ 𝑀 = (mulGrp‘𝑆)
251		evlsbagval.e	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘𝑀)
252	52	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → 𝑆 ∈ Ring)
253		ovexd 7190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝐾 ↑_m 𝐼) ∈ V)
254	230	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝐵‘𝑣) ∈ ℕ₀)
255	235	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
256	38, 50, 39, 250, 40, 251, 252, 253, 254, 255, 246	pwsexpg 39803	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))‘𝑙) = ((𝐵‘𝑣) ↑ ((𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))‘𝑙)))
257		fveq1 6661	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑙 → (𝑔‘𝑣) = (𝑙‘𝑣))
258	257	oveq2d 7171	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑙 → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = ((𝐵‘𝑣) ↑ (𝑙‘𝑣)))
259		ovexd 7190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ (𝑙‘𝑣)) ∈ V)
260	241, 258, 246, 259	fvmptd3 6786	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → ((𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))‘𝑙) = ((𝐵‘𝑣) ↑ (𝑙‘𝑣)))
261	249, 256, 260	3eqtr4d 2803	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐼) ∧ 𝑙 ∈ (𝐾 ↑_m 𝐼)) → (((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))‘𝑙) = ((𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))‘𝑙))
262	239, 243, 261	eqfnfvd 6800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))
263	262	mpteq2dva 5130	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣)(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑣)))) = (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))))
264	224, 263	eqtrd 2793	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))))
265	264	oveq2d 7171	. . . . . 6 ⊢ (𝜑 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝐵 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))) = ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))))
266	250	crngmgp 19378	. . . . . . . . . . 11 ⊢ (𝑆 ∈ CRing → 𝑀 ∈ CMnd)
267	45, 266	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ CMnd)
268	267	cmnmndd 19001	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ Mnd)
269	268	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → 𝑀 ∈ Mnd)
270	230	adantrl 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → (𝐵‘𝑣) ∈ ℕ₀)
271		elmapi 8443	. . . . . . . . . 10 ⊢ (𝑔 ∈ (𝐾 ↑_m 𝐼) → 𝑔:𝐼⟶𝐾)
272	271	ad2antrl 727	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → 𝑔:𝐼⟶𝐾)
273		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → 𝑣 ∈ 𝐼)
274	272, 273	ffvelrnd 6848	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → (𝑔‘𝑣) ∈ 𝐾)
275	250, 37	mgpbas 19318	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑀)
276	275, 251	mulgnn0cl 18316	. . . . . . . 8 ⊢ ((𝑀 ∈ Mnd ∧ (𝐵‘𝑣) ∈ ℕ₀ ∧ (𝑔‘𝑣) ∈ 𝐾) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) ∈ 𝐾)
277	269, 270, 274, 276	syl3anc 1368	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐾 ↑_m 𝐼) ∧ 𝑣 ∈ 𝐼)) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) ∈ 𝐾)
278	23	mptexd 6983	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) ∈ V)
279		fvexd 6677	. . . . . . . 8 ⊢ (𝜑 → (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) ∈ V)
280		funmpt 6377	. . . . . . . . 9 ⊢ Fun (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))
281	280	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Fun (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))))
282	2	psrbagfsupp 20687	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐷 → 𝐵 finSupp 0)
283	161, 282	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 finSupp 0)
284	283	fsuppimpd 8878	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 supp 0) ∈ Fin)
285		ssidd 3917	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 supp 0) ⊆ (𝐵 supp 0))
286		c0ex 10678	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
287	286	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ V)
288	211, 285, 23, 287	suppssr 7875	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐵‘𝑣) = 0)
289	288	oveq1d 7170	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = (0 ↑ (𝑔‘𝑣)))
290	289	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = (0 ↑ (𝑔‘𝑣)))
291	271	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → 𝑔:𝐼⟶𝐾)
292		eldifi 4034	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝐼 ∖ (𝐵 supp 0)) → 𝑣 ∈ 𝐼)
293	292	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → 𝑣 ∈ 𝐼)
294	291, 293	ffvelrnd 6848	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → (𝑔‘𝑣) ∈ 𝐾)
295	250, 68	ringidval 19326	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑆) = (0_g‘𝑀)
296	275, 295, 251	mulg0 18303	. . . . . . . . . . . . . 14 ⊢ ((𝑔‘𝑣) ∈ 𝐾 → (0 ↑ (𝑔‘𝑣)) = (1_r‘𝑆))
297	294, 296	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → (0 ↑ (𝑔‘𝑣)) = (1_r‘𝑆))
298	290, 297	eqtrd 2793	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) ∧ 𝑔 ∈ (𝐾 ↑_m 𝐼)) → ((𝐵‘𝑣) ↑ (𝑔‘𝑣)) = (1_r‘𝑆))
299	298	mpteq2dva 5130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (1_r‘𝑆)))
300		fconstmpt 5587	. . . . . . . . . . . 12 ⊢ ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (1_r‘𝑆))
301		ovexd 7190	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝐾 ↑_m 𝐼) ∈ V)
302	52, 301, 186	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → ((𝐾 ↑_m 𝐼) × {(1_r‘𝑆)}) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
303	300, 302	syl5eqr 2807	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (1_r‘𝑆)) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
304	299, 303	eqtrd 2793	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝐼 ∖ (𝐵 supp 0))) → (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))) = (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
305	304, 23	suppss2 7879	. . . . . . . . 9 ⊢ (𝜑 → ((𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) supp (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ⊆ (𝐵 supp 0))
306	284, 305	ssfid 8783	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) supp (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) ∈ Fin)
307	278, 279, 281, 306	isfsuppd 39752	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣)))) finSupp (1_r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
308	38, 37, 199, 39, 250, 53, 23, 45, 277, 307	pwsgprod 39804	. . . . . 6 ⊢ (𝜑 → ((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑣 ∈ 𝐼 ↦ (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))) = (𝑔 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝑔‘𝑣))))))
309	201, 265, 308	3eqtrd 2797	. . . . 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 2797	. . . 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 7190	. . . 4 ⊢ (𝜑 → (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ V)
313	170, 310, 311, 312	fvmptd4 39745	. . 3 ⊢ (𝜑 → (((𝑆 ↑_s (𝐾 ↑_m 𝐼)) Σ_g (𝑏 ∈ {𝐵} ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑_m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(._r‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))((mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) Σ_g (𝑏 ∘_f (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑_m 𝐼) ↦ (𝑎‘𝑥))))))))‘𝐴) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))
314	49, 166, 313	3eqtrd 2797	. 2 ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))
315	30, 314	jca 515	1 ⊢ (𝜑 → (𝐹 ∈ 𝑊 ∧ ((𝑄‘𝐹)‘𝐴) = (𝑀 Σ_g (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 {crab 3074 Vcvv 3409 ∖ cdif 3857 ⊆ wss 3860 ifcif 4423 {csn 4525 class class class wbr 5035 ↦ cmpt 5115 × cxp 5525 ^◡ccnv 5526 ↾ cres 5529 “ cima 5530 Fun wfun 6333 Fn wfn 6334 ⟶wf 6335 ‘cfv 6339 (class class class)co 7155 ∘_f cof 7408 supp csupp 7840 ↑_m cmap 8421 Fincfn 8532 finSupp cfsupp 8871 0cc0 10580 ℕcn 11679 ℕ₀cn0 11939 Basecbs 16546 ↾_s cress 16547 ._rcmulr 16629 0_gc0g 16776 Σ_g cgsu 16777 ↑_s cpws 16783 Mndcmnd 17982 ._gcmg 18296 CMndccmn 18978 mulGrpcmgp 19312 1_rcur 19324 Ringcrg 19370 CRingccrg 19371 SubRingcsubrg 19604 mPwSer cmps 20671 mPoly cmpl 20673 evalSub ces 20838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 ax-cnex 10636 ax-resscn 10637 ax-1cn 10638 ax-icn 10639 ax-addcl 10640 ax-addrcl 10641 ax-mulcl 10642 ax-mulrcl 10643 ax-mulcom 10644 ax-addass 10645 ax-mulass 10646 ax-distr 10647 ax-i2m1 10648 ax-1ne0 10649 ax-1rid 10650 ax-rnegex 10651 ax-rrecex 10652 ax-cnre 10653 ax-pre-lttri 10654 ax-pre-lttrn 10655 ax-pre-ltadd 10656 ax-pre-mulgt0 10657

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-iin 4889 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-se 5487 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-of 7410 df-ofr 7411 df-om 7585 df-1st 7698 df-2nd 7699 df-supp 7841 df-wrecs 7962 df-recs 8023 df-rdg 8061 df-1o 8117 df-er 8304 df-map 8423 df-pm 8424 df-ixp 8485 df-en 8533 df-dom 8534 df-sdom 8535 df-fin 8536 df-fsupp 8872 df-sup 8944 df-oi 9012 df-card 9406 df-pnf 10720 df-mnf 10721 df-xr 10722 df-ltxr 10723 df-le 10724 df-sub 10915 df-neg 10916 df-nn 11680 df-2 11742 df-3 11743 df-4 11744 df-5 11745 df-6 11746 df-7 11747 df-8 11748 df-9 11749 df-n0 11940 df-z 12026 df-dec 12143 df-uz 12288 df-fz 12945 df-fzo 13088 df-seq 13424 df-hash 13746 df-struct 16548 df-ndx 16549 df-slot 16550 df-base 16552 df-sets 16553 df-ress 16554 df-plusg 16641 df-mulr 16642 df-sca 16644 df-vsca 16645 df-ip 16646 df-tset 16647 df-ple 16648 df-ds 16650 df-hom 16652 df-cco 16653 df-0g 16778 df-gsum 16779 df-prds 16784 df-pws 16786 df-mre 16920 df-mrc 16921 df-acs 16923 df-mgm 17923 df-sgrp 17972 df-mnd 17983 df-mhm 18027 df-submnd 18028 df-grp 18177 df-minusg 18178 df-sbg 18179 df-mulg 18297 df-subg 18348 df-ghm 18428 df-cntz 18519 df-cmn 18980 df-abl 18981 df-mgp 19313 df-ur 19325 df-srg 19329 df-ring 19372 df-cring 19373 df-rnghom 19543 df-subrg 19606 df-lmod 19709 df-lss 19777 df-lsp 19817 df-assa 20623 df-asp 20624 df-ascl 20625 df-psr 20676 df-mvr 20677 df-mpl 20678 df-evls 20840

This theorem is referenced by: mhphf 39818

W3C validator