Theorem mhphf 40285

Description: A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the (𝑄‘𝑋) which corresponds to 𝑋). (Contributed by SN, 28-Jul-2024.)

Hypotheses

Ref	Expression
mhphf.q	⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
mhphf.h	⊢ 𝐻 = (𝐼 mHomP 𝑈)
mhphf.u	⊢ 𝑈 = (𝑆 ↾s 𝑅)
mhphf.k	⊢ 𝐾 = (Base‘𝑆)
mhphf.m	⊢ · = (.r‘𝑆)
mhphf.e	⊢ ↑ = (.g‘(mulGrp‘𝑆))
mhphf.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
mhphf.s	⊢ (𝜑 → 𝑆 ∈ CRing)
mhphf.r	⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
mhphf.l	⊢ (𝜑 → 𝐿 ∈ 𝑅)
mhphf.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
mhphf.x	⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
mhphf.a	⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))

Assertion

Ref	Expression
mhphf	⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))

Proof of Theorem mhphf

Dummy variables 𝑎 𝑏 𝑓 𝑠 𝑗 𝑘 𝑣 𝑥 𝑦 ℎ 𝑤 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mhphf.h	. . 3 ⊢ 𝐻 = (𝐼 mHomP 𝑈)
2		eqid 2738	. . 3 ⊢ (Base‘𝑈) = (Base‘𝑈)
3		eqid 2738	. . 3 ⊢ (0g‘𝑈) = (0g‘𝑈)
4		eqid 2738	. . 3 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈)
5		eqid 2738	. . 3 ⊢ (+g‘(𝐼 mPoly 𝑈)) = (+g‘(𝐼 mPoly 𝑈))
6		eqid 2738	. . 3 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
7		eqid 2738	. . 3 ⊢ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} = {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}
8		mhphf.i	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
9		mhphf.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
10		mhphf.u	. . . . . 6 ⊢ 𝑈 = (𝑆 ↾s 𝑅)
11	10	subrgring 20027	. . . . 5 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
12	9, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ∈ Ring)
13	12	ringgrpd 19792	. . 3 ⊢ (𝜑 → 𝑈 ∈ Grp)
14		mhphf.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
15		mhphf.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
16		eqid 2738	. . . . . 6 ⊢ (algSc‘(𝐼 mPoly 𝑈)) = (algSc‘(𝐼 mPoly 𝑈))
17		eqid 2738	. . . . . 6 ⊢ (0g‘(𝐼 mPoly 𝑈)) = (0g‘(𝐼 mPoly 𝑈))
18		mhphf.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ CRing)
19	10	subrgcrng 20028	. . . . . . 7 ⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing)
20	18, 9, 19	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ CRing)
21	4, 16, 3, 17, 8, 20	mplascl0 40270	. . . . 5 ⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) = (0g‘(𝐼 mPoly 𝑈)))
22	4, 6, 3, 17, 8, 13	mpl0 21212	. . . . 5 ⊢ (𝜑 → (0g‘(𝐼 mPoly 𝑈)) = ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝑈)}))
23	21, 22	eqtr2d 2779	. . . 4 ⊢ (𝜑 → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝑈)}) = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))
24		mhphf.m	. . . . . . . . . 10 ⊢ · = (.r‘𝑆)
25	10, 24	ressmulr 17017	. . . . . . . . 9 ⊢ (𝑅 ∈ (SubRing‘𝑆) → · = (.r‘𝑈))
26	9, 25	syl 17	. . . . . . . 8 ⊢ (𝜑 → · = (.r‘𝑈))
27	26	oveqd 7292	. . . . . . 7 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · (0g‘𝑈)) = ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)))
28		eqid 2738	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
29	28	subrgsubm 20037	. . . . . . . . . . 11 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)))
30	9, 29	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)))
31		mhphf.l	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
32		mhphf.e	. . . . . . . . . . 11 ⊢ ↑ = (.g‘(mulGrp‘𝑆))
33	32	submmulgcl 18746	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)) ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ 𝑅) → (𝑁 ↑ 𝐿) ∈ 𝑅)
34	30, 14, 31, 33	syl3anc 1370	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝑅)
35	10	subrgbas 20033	. . . . . . . . . 10 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
36	9, 35	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 = (Base‘𝑈))
37	34, 36	eleqtrd 2841	. . . . . . . 8 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ (Base‘𝑈))
38		eqid 2738	. . . . . . . . 9 ⊢ (.r‘𝑈) = (.r‘𝑈)
39	2, 38, 3	ringrz 19827	. . . . . . . 8 ⊢ ((𝑈 ∈ Ring ∧ (𝑁 ↑ 𝐿) ∈ (Base‘𝑈)) → ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈))
40	12, 37, 39	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈))
41	27, 40	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · (0g‘𝑈)) = (0g‘𝑈))
42		mhphf.q	. . . . . . . . 9 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
43		mhphf.k	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑆)
44		eqid 2738	. . . . . . . . 9 ⊢ (Base‘(𝐼 mPoly 𝑈)) = (Base‘(𝐼 mPoly 𝑈))
45	2, 3	ring0cl 19808	. . . . . . . . . . 11 ⊢ (𝑈 ∈ Ring → (0g‘𝑈) ∈ (Base‘𝑈))
46	12, 45	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑈) ∈ (Base‘𝑈))
47	46, 36	eleqtrrd 2842	. . . . . . . . 9 ⊢ (𝜑 → (0g‘𝑈) ∈ 𝑅)
48		mhphf.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))
49	42, 4, 10, 43, 44, 16, 8, 18, 9, 47, 48	evlsscaval 40273	. . . . . . . 8 ⊢ (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴) = (0g‘𝑈)))
50	49	simprd 496	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴) = (0g‘𝑈))
51	50	oveq2d 7291	. . . . . 6 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)) = ((𝑁 ↑ 𝐿) · (0g‘𝑈)))
52	43	fvexi 6788	. . . . . . . . . 10 ⊢ 𝐾 ∈ V
53	52	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ V)
54	18	crngringd 19796	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Ring)
55	43, 24	ringcl 19800	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
56	54, 55	syl3an1 1162	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
57	56	3expb 1119	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
58	43	subrgss 20025	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾)
59	9, 58	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⊆ 𝐾)
60	59, 31	sseldd 3922	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ 𝐾)
61		fconst6g 6663	. . . . . . . . . . 11 ⊢ (𝐿 ∈ 𝐾 → (𝐼 × {𝐿}):𝐼⟶𝐾)
62	60, 61	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝐾)
63		elmapi 8637	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐾 ↑m 𝐼) → 𝐴:𝐼⟶𝐾)
64	48, 63	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:𝐼⟶𝐾)
65		inidm 4152	. . . . . . . . . 10 ⊢ (𝐼 ∩ 𝐼) = 𝐼
66	57, 62, 64, 8, 8, 65	off 7551	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾)
67	53, 8, 66	elmapdd 40216	. . . . . . . 8 ⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼))
68	42, 4, 10, 43, 44, 16, 8, 18, 9, 47, 67	evlsscaval 40273	. . . . . . 7 ⊢ (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g‘𝑈)))
69	68	simprd 496	. . . . . 6 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g‘𝑈))
70	41, 51, 69	3eqtr4rd 2789	. . . . 5 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)))
71		fvex 6787	. . . . . 6 ⊢ ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ V
72		fveq2 6774	. . . . . . . 8 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → (𝑄‘𝑓) = (𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈))))
73	72	fveq1d 6776	. . . . . . 7 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
74	72	fveq1d 6776	. . . . . . . 8 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))
75	74	oveq2d 7291	. . . . . . 7 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)))
76	73, 75	eqeq12d 2754	. . . . . 6 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))))
77	71, 76	elab 3609	. . . . 5 ⊢ (((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)))
78	70, 77	sylibr 233	. . . 4 ⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
79	23, 78	eqeltrd 2839	. . 3 ⊢ (𝜑 → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝑈)}) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
80	4	mplassa 21227	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑈 ∈ CRing) → (𝐼 mPoly 𝑈) ∈ AssAlg)
81	8, 20, 80	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐼 mPoly 𝑈) ∈ AssAlg)
82	81	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 mPoly 𝑈) ∈ AssAlg)
83	4, 8, 12	mplsca 21217	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 = (Scalar‘(𝐼 mPoly 𝑈)))
84	83	fveq2d 6778	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑈) = (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
85	84	eleq2d 2824	. . . . . . . . 9 ⊢ (𝜑 → (𝑏 ∈ (Base‘𝑈) ↔ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈)))))
86	85	biimpa 477	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
87	86	adantrl 713	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
88		fvexd 6789	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑈) ∈ V)
89		ovex 7308	. . . . . . . . . . . . 13 ⊢ (ℕ0 ↑m 𝐼) ∈ V
90	89	rabex 5256	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V)
92		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑈) = (1r‘𝑈)
93	2, 92	ringidcl 19807	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ Ring → (1r‘𝑈) ∈ (Base‘𝑈))
94	12, 93	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝑈) ∈ (Base‘𝑈))
95	94, 46	ifcld 4505	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ (Base‘𝑈))
96	95	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ (Base‘𝑈))
97	96	fmpttd 6989	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))):{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑈))
98	88, 91, 97	elmapdd 40216	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ ((Base‘𝑈) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}))
99		eqid 2738	. . . . . . . . . . 11 ⊢ (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
100		eqid 2738	. . . . . . . . . . 11 ⊢ (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
101	99, 2, 6, 100, 8	psrbas 21147	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}))
102	98, 101	eleqtrrd 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)))
103	90	mptex 7099	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ V
104	103	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ V)
105		fvexd 6789	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑈) ∈ V)
106		funmpt 6472	. . . . . . . . . . 11 ⊢ Fun (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
107	106	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))
108		snfi 8834	. . . . . . . . . . . 12 ⊢ {𝑎} ∈ Fin
109	108	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎} ∈ Fin)
110		eldifsnneq 4724	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎}) → ¬ 𝑤 = 𝑎)
111	110	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎})) → ¬ 𝑤 = 𝑎)
112	111	iffalsed 4470	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎})) → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) = (0g‘𝑈))
113	112, 91	suppss2 8016	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) supp (0g‘𝑈)) ⊆ {𝑎})
114	109, 113	ssfid 9042	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) supp (0g‘𝑈)) ∈ Fin)
115	104, 105, 107, 114	isfsuppd 40217	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) finSupp (0g‘𝑈))
116	4, 99, 100, 3, 44	mplelbas 21199	. . . . . . . . 9 ⊢ ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ↔ ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) finSupp (0g‘𝑈)))
117	102, 115, 116	sylanbrc 583	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)))
118	117	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)))
119		eqid 2738	. . . . . . . 8 ⊢ (Scalar‘(𝐼 mPoly 𝑈)) = (Scalar‘(𝐼 mPoly 𝑈))
120		eqid 2738	. . . . . . . 8 ⊢ (Base‘(Scalar‘(𝐼 mPoly 𝑈))) = (Base‘(Scalar‘(𝐼 mPoly 𝑈)))
121		eqid 2738	. . . . . . . 8 ⊢ (.r‘(𝐼 mPoly 𝑈)) = (.r‘(𝐼 mPoly 𝑈))
122		eqid 2738	. . . . . . . 8 ⊢ ( ·𝑠 ‘(𝐼 mPoly 𝑈)) = ( ·𝑠 ‘(𝐼 mPoly 𝑈))
123	16, 119, 120, 44, 121, 122	asclmul1 21090	. . . . . . 7 ⊢ (((𝐼 mPoly 𝑈) ∈ AssAlg ∧ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))) ∧ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))
124	82, 87, 118, 123	syl3anc 1370	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))
125		simprr 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘𝑈))
126	4, 122, 2, 44, 38, 6, 125, 118	mplvsca 21219	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r‘𝑈)(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))
127	124, 126	eqtrd 2778	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r‘𝑈)(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))
128		vex 3436	. . . . . . 7 ⊢ 𝑏 ∈ V
129		fnconstg 6662	. . . . . . 7 ⊢ (𝑏 ∈ V → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) Fn {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
130	128, 129	mp1i 13	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) Fn {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
131		fvex 6787	. . . . . . . . 9 ⊢ (1r‘𝑈) ∈ V
132		fvex 6787	. . . . . . . . 9 ⊢ (0g‘𝑈) ∈ V
133	131, 132	ifex 4509	. . . . . . . 8 ⊢ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ V
134		eqid 2738	. . . . . . . 8 ⊢ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
135	133, 134	fnmpti 6576	. . . . . . 7 ⊢ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) Fn {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
136	135	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) Fn {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
137	90	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V)
138		inidm 4152	. . . . . 6 ⊢ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∩ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
139	128	fvconst2 7079	. . . . . . 7 ⊢ (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} → (({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏)
140	139	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏)
141		equequ1 2028	. . . . . . . . 9 ⊢ (𝑤 = 𝑠 → (𝑤 = 𝑎 ↔ 𝑠 = 𝑎))
142	141	ifbid 4482	. . . . . . . 8 ⊢ (𝑤 = 𝑠 → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
143	131, 132	ifex 4509	. . . . . . . 8 ⊢ if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ V
144	142, 134, 143	fvmpt 6875	. . . . . . 7 ⊢ (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
145	144	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
146	130, 136, 137, 137, 138, 140, 145	offval 7542	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r‘𝑈)(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))
147		ovif2 7373	. . . . . . 7 ⊢ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = if(𝑠 = 𝑎, (𝑏(.r‘𝑈)(1r‘𝑈)), (𝑏(.r‘𝑈)(0g‘𝑈)))
148	12	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑈 ∈ Ring)
149		simplrr 775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑏 ∈ (Base‘𝑈))
150	2, 38, 92, 148, 149	ringridmd 40243	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)(1r‘𝑈)) = 𝑏)
151	2, 38, 3	ringrz 19827	. . . . . . . . 9 ⊢ ((𝑈 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑈)) → (𝑏(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈))
152	148, 149, 151	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈))
153	150, 152	ifeq12d 4480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → if(𝑠 = 𝑎, (𝑏(.r‘𝑈)(1r‘𝑈)), (𝑏(.r‘𝑈)(0g‘𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g‘𝑈)))
154	147, 153	eqtrid 2790	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g‘𝑈)))
155	154	mpteq2dva 5174	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))))
156	127, 146, 155	3eqtrd 2782	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))))
157	8	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐼 ∈ 𝑉)
158	18	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ CRing)
159	9	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑅 ∈ (SubRing‘𝑆))
160	67	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼))
161	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑈 ∈ Ring)
162	4, 44, 2, 16, 157, 161	mplasclf 21273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (algSc‘(𝐼 mPoly 𝑈)):(Base‘𝑈)⟶(Base‘(𝐼 mPoly 𝑈)))
163	162, 125	ffvelrnd 6962	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)))
164		eqidd 2739	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
165	163, 164	jca 512	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴))))
166		elrabi 3618	. . . . . . . . . 10 ⊢ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
167	166	ad2antrl 725	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
168	42, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 160, 167	evlsbagval 40275	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))
169	42, 4, 10, 43, 44, 157, 158, 159, 160, 165, 168, 121, 24	evlsmulval 40278	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))))))
170	169	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))
171	28	ringmgp 19789	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
172	54, 171	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
173	28, 43	mgpbas 19726	. . . . . . . . . . . . 13 ⊢ 𝐾 = (Base‘(mulGrp‘𝑆))
174	173, 32	mulgnn0cl 18720	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑆) ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ 𝐾) → (𝑁 ↑ 𝐿) ∈ 𝐾)
175	172, 14, 60, 174	syl3anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝐾)
176	175	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑁 ↑ 𝐿) ∈ 𝐾)
177	36, 59	eqsstrrd 3960	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾)
178	177	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ 𝐾)
179	178	adantrl 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ 𝐾)
180	43, 24	crngcom 19801	. . . . . . . . . 10 ⊢ ((𝑆 ∈ CRing ∧ (𝑁 ↑ 𝐿) ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → ((𝑁 ↑ 𝐿) · 𝑏) = (𝑏 · (𝑁 ↑ 𝐿)))
181	158, 176, 179, 180	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · 𝑏) = (𝑏 · (𝑁 ↑ 𝐿)))
182	181	oveq1d 7290	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 ↑ 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑏 · (𝑁 ↑ 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
183	158	crngringd 19796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ Ring)
184		eqid 2738	. . . . . . . . . . 11 ⊢ (1r‘𝑆) = (1r‘𝑆)
185	28, 184	ringidval 19739	. . . . . . . . . 10 ⊢ (1r‘𝑆) = (0g‘(mulGrp‘𝑆))
186	28	crngmgp 19791	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CRing → (mulGrp‘𝑆) ∈ CMnd)
187	18, 186	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ CMnd)
188	187	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (mulGrp‘𝑆) ∈ CMnd)
189	172	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd)
190		elrabi 3618	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑎 ∈ (ℕ0 ↑m 𝐼))
191		elmapi 8637	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (ℕ0 ↑m 𝐼) → 𝑎:𝐼⟶ℕ0)
192	166, 190, 191	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎:𝐼⟶ℕ0)
193	192	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝑎:𝐼⟶ℕ0)
194	193	adantrr 714	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎:𝐼⟶ℕ0)
195	194	ffvelrnda 6961	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈ ℕ0)
196	64	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐴:𝐼⟶𝐾)
197		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
198	196, 197	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾)
199	173, 32	mulgnn0cl 18720	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑆) ∈ Mnd ∧ (𝑎‘𝑣) ∈ ℕ0 ∧ (𝐴‘𝑣) ∈ 𝐾) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾)
200	189, 195, 198, 199	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾)
201	200	fmpttd 6989	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))):𝐼⟶𝐾)
202	6	psrbagfsupp 21123	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑎 finSupp 0)
203	202	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑎 finSupp 0)
204	203	fsuppimpd 9135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑎 supp 0) ∈ Fin)
205	166, 204	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ∈ Fin)
206	205	adantrr 714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ∈ Fin)
207	194	feqmptd 6837	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)))
208	207	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) = ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0))
209		ssidd 3944	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
210	208, 209	eqsstrrd 3960	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0) ⊆ (𝑎 supp 0))
211	173, 185, 32	mulg0 18707	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐾 → (0 ↑ 𝑘) = (1r‘𝑆))
212	211	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆))
213		c0ex 10969	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
214	213	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 0 ∈ V)
215	210, 212, 195, 198, 214	suppssov1 8014	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ⊆ (𝑎 supp 0))
216	206, 215	ssfid 9042	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ∈ Fin)
217	173, 185, 188, 157, 201, 216	gsumcl2 19515	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾)
218	43, 24, 183, 176, 179, 217	ringassd 40241	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 ↑ 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
219	43, 24, 183, 179, 176, 217	ringassd 40241	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑏 · (𝑁 ↑ 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = (𝑏 · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
220	182, 218, 219	3eqtr3d 2786	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) = (𝑏 · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
221	48	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 ∈ (𝐾 ↑m 𝐼))
222	36	eleq2d 2824	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑏 ∈ 𝑅 ↔ 𝑏 ∈ (Base‘𝑈)))
223	222	biimpar 478	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ 𝑅)
224	223	adantrl 713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ 𝑅)
225	42, 4, 10, 43, 44, 16, 157, 158, 159, 224, 221	evlsscaval 40273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘𝐴) = 𝑏))
226	42, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 221, 167	evlsbagval 40275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))‘𝐴) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
227	42, 4, 10, 43, 44, 157, 158, 159, 221, 225, 226, 121, 24	evlsmulval 40278	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴) = (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
228	227	simprd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴) = (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
229	228	oveq2d 7291	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)) = ((𝑁 ↑ 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
230	42, 4, 10, 43, 44, 16, 157, 158, 159, 224, 160	evlsscaval 40273	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏))
231	230	simprd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏)
232		fconst6g 6663	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ 𝑅 → (𝐼 × {𝐿}):𝐼⟶𝑅)
233	31, 232	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝑅)
234	233	ffnd 6601	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 × {𝐿}) Fn 𝐼)
235	234	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 × {𝐿}) Fn 𝐼)
236	64	ffnd 6601	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 Fn 𝐼)
237	236	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 Fn 𝐼)
238	31	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝑅)
239		fvconst2g 7077	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ 𝑅 ∧ 𝑣 ∈ 𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
240	238, 197, 239	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
241		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) = (𝐴‘𝑣))
242	235, 237, 157, 157, 65, 240, 241	ofval 7544	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣) = (𝐿 · (𝐴‘𝑣)))
243	242	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))))
244	187	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ CMnd)
245	60	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝐾)
246	28, 24	mgpplusg 19724	. . . . . . . . . . . . . 14 ⊢ · = (+g‘(mulGrp‘𝑆))
247	173, 32, 246	mulgnn0di 19427	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘𝑆) ∈ CMnd ∧ ((𝑎‘𝑣) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ (𝐴‘𝑣) ∈ 𝐾)) → ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
248	244, 195, 245, 198, 247	syl13anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
249	243, 248	eqtrd 2778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
250	249	mpteq2dva 5174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))
251	250	oveq2d 7291	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
252	187	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd)
253	8	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝐼 ∈ 𝑉)
254	172	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd)
255	193	ffvelrnda 6961	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈ ℕ0)
256	60	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝐾)
257	173, 32	mulgnn0cl 18720	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘𝑆) ∈ Mnd ∧ (𝑎‘𝑣) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾) → ((𝑎‘𝑣) ↑ 𝐿) ∈ 𝐾)
258	254, 255, 256, 257	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ 𝐿) ∈ 𝐾)
259	64	ffvelrnda 6961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾)
260	259	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾)
261	254, 255, 260, 199	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾)
262		eqidd 2739	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) = (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)))
263		eqidd 2739	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) = (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
264	253	mptexd 7100	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) ∈ V)
265		fvexd 6789	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (1r‘𝑆) ∈ V)
266		funmpt 6472	. . . . . . . . . . . . . 14 ⊢ Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))
267	266	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)))
268	193	feqmptd 6837	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)))
269	268	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) = ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0))
270		ssidd 3944	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
271	269, 270	eqsstrrd 3960	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0) ⊆ (𝑎 supp 0))
272	211	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆))
273	213	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 0 ∈ V)
274	271, 272, 255, 256, 273	suppssov1 8014	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) supp (1r‘𝑆)) ⊆ (𝑎 supp 0))
275	205, 274	ssfid 9042	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) supp (1r‘𝑆)) ∈ Fin)
276	264, 265, 267, 275	isfsuppd 40217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) finSupp (1r‘𝑆))
277	253	mptexd 7100	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) ∈ V)
278		funmpt 6472	. . . . . . . . . . . . . 14 ⊢ Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))
279	278	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
280	271, 272, 255, 260, 273	suppssov1 8014	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ⊆ (𝑎 supp 0))
281	205, 280	ssfid 9042	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ∈ Fin)
282	277, 265, 279, 281	isfsuppd 40217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) finSupp (1r‘𝑆))
283	173, 185, 246, 252, 253, 258, 261, 262, 263, 276, 282	gsummptfsadd 19525	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = (((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
284	6, 7, 173, 32, 8, 172, 60, 14	mhphflem 40284	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) = (𝑁 ↑ 𝐿))
285	284	oveq1d 7290	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
286	283, 285	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
287	286	adantrr 714	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
288	251, 287	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
289	231, 288	oveq12d 7293	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = (𝑏 · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
290	220, 229, 289	3eqtr4rd 2789	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)))
291	170, 290	eqtrd 2778	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)))
292		ovex 7308	. . . . . 6 ⊢ (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ V
293		fveq2 6774	. . . . . . . 8 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → (𝑄‘𝑓) = (𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))))
294	293	fveq1d 6776	. . . . . . 7 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
295	293	fveq1d 6776	. . . . . . . 8 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))
296	295	oveq2d 7291	. . . . . . 7 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)))
297	294, 296	eqeq12d 2754	. . . . . 6 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))))
298	292, 297	elab 3609	. . . . 5 ⊢ ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)))
299	291, 298	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
300	156, 299	eqeltrrd 2840	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
301		elin 3903	. . . . . 6 ⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))
302		vex 3436	. . . . . . . 8 ⊢ 𝑥 ∈ V
303		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑓 = 𝑥 → (𝑄‘𝑓) = (𝑄‘𝑥))
304	303	fveq1d 6776	. . . . . . . . 9 ⊢ (𝑓 = 𝑥 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
305	303	fveq1d 6776	. . . . . . . . . 10 ⊢ (𝑓 = 𝑥 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑥)‘𝐴))
306	305	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑓 = 𝑥 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))
307	304, 306	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑓 = 𝑥 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
308	302, 307	elab 3609	. . . . . . 7 ⊢ (𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))
309	308	anbi2i 623	. . . . . 6 ⊢ ((𝑥 ∈ (𝐻‘𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
310	301, 309	bitri 274	. . . . 5 ⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
311		elin 3903	. . . . . 6 ⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))
312		vex 3436	. . . . . . . 8 ⊢ 𝑦 ∈ V
313		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑓 = 𝑦 → (𝑄‘𝑓) = (𝑄‘𝑦))
314	313	fveq1d 6776	. . . . . . . . 9 ⊢ (𝑓 = 𝑦 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
315	313	fveq1d 6776	. . . . . . . . . 10 ⊢ (𝑓 = 𝑦 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑦)‘𝐴))
316	315	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑓 = 𝑦 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))
317	314, 316	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑓 = 𝑦 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
318	312, 317	elab 3609	. . . . . . 7 ⊢ (𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))
319	318	anbi2i 623	. . . . . 6 ⊢ ((𝑦 ∈ (𝐻‘𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
320	311, 319	bitri 274	. . . . 5 ⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
321	310, 320	anbi12i 627	. . . 4 ⊢ ((𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})) ↔ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))))
322	54	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑆 ∈ Ring)
323	175	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑁 ↑ 𝐿) ∈ 𝐾)
324		eqid 2738	. . . . . . . . 9 ⊢ (𝑆 ↑s (Base‘(𝑆 ↑s 𝐼))) = (𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))
325		eqid 2738	. . . . . . . . 9 ⊢ (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))) = (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼))))
326	18	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑆 ∈ CRing)
327		fvexd 6789	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (Base‘(𝑆 ↑s 𝐼)) ∈ V)
328		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ↑s (𝐾 ↑m 𝐼)) = (𝑆 ↑s (𝐾 ↑m 𝐼))
329	42, 4, 10, 328, 43	evlsrhm 21298	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))))
330	8, 18, 9, 329	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))))
331		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))
332	44, 331	rhmf 19970	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
333	330, 332	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
334	333	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
335	8	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝐼 ∈ 𝑉)
336	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑈 ∈ Ring)
337	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑁 ∈ ℕ0)
338		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑥 ∈ (𝐻‘𝑁))
339	1, 4, 44, 335, 336, 337, 338	mhpmpl 21334	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
340	339	adantrr 714	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
341	340	adantrr 714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
342	334, 341	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
343		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ↑s 𝐼) = (𝑆 ↑s 𝐼)
344	343, 43	pwsbas 17198	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ CRing ∧ 𝐼 ∈ 𝑉) → (𝐾 ↑m 𝐼) = (Base‘(𝑆 ↑s 𝐼)))
345	18, 8, 344	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ↑m 𝐼) = (Base‘(𝑆 ↑s 𝐼)))
346	345	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ↑s (𝐾 ↑m 𝐼)) = (𝑆 ↑s (Base‘(𝑆 ↑s 𝐼))))
347	346	fveq2d 6778	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
348	347	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
349	342, 348	eleqtrd 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥) ∈ (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
350	324, 43, 325, 326, 327, 349	pwselbas 17200	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥):(Base‘(𝑆 ↑s 𝐼))⟶𝐾)
351	48, 345	eleqtrd 2841	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Base‘(𝑆 ↑s 𝐼)))
352	351	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴 ∈ (Base‘(𝑆 ↑s 𝐼)))
353	350, 352	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘𝑥)‘𝐴) ∈ 𝐾)
354	8	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝐼 ∈ 𝑉)
355	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑈 ∈ Ring)
356	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑁 ∈ ℕ0)
357		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑦 ∈ (𝐻‘𝑁))
358	1, 4, 44, 354, 355, 356, 357	mhpmpl 21334	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
359	358	adantrr 714	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
360	359	adantrl 713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
361	334, 360	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
362	361, 348	eleqtrd 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦) ∈ (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
363	324, 43, 325, 326, 327, 362	pwselbas 17200	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦):(Base‘(𝑆 ↑s 𝐼))⟶𝐾)
364	363, 352	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘𝑦)‘𝐴) ∈ 𝐾)
365		eqid 2738	. . . . . . . 8 ⊢ (+g‘𝑆) = (+g‘𝑆)
366	43, 365, 24	ringdi 19805	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ ((𝑁 ↑ 𝐿) ∈ 𝐾 ∧ ((𝑄‘𝑥)‘𝐴) ∈ 𝐾 ∧ ((𝑄‘𝑦)‘𝐴) ∈ 𝐾)) → ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
367	322, 323, 353, 364, 366	syl13anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
368	8	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐼 ∈ 𝑉)
369	9	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑅 ∈ (SubRing‘𝑆))
370	48	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴 ∈ (𝐾 ↑m 𝐼))
371		eqidd 2739	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) → ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴))
372	339, 371	anim12dan 619	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴)))
373	372	adantrr 714	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴)))
374		eqidd 2739	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) → ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴))
375	358, 374	anim12dan 619	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴)))
376	375	adantrl 713	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴)))
377	42, 4, 10, 43, 44, 368, 326, 369, 370, 373, 376, 5, 365	evlsaddval 40277	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))))
378	377	simprd 496	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴)))
379	378	oveq2d 7291	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)) = ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))))
380	52	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐾 ∈ V)
381	57	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
382	62	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝐼 × {𝐿}):𝐼⟶𝐾)
383	64	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴:𝐼⟶𝐾)
384	381, 382, 383, 368, 368, 65	off 7551	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾)
385	380, 368, 384	elmapdd 40216	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼))
386		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) → ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))
387	339, 386	anim12dan 619	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
388	387	adantrr 714	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
389		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) → ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))
390	358, 389	anim12dan 619	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
391	390	adantrl 713	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
392	42, 4, 10, 43, 44, 368, 326, 369, 385, 388, 391, 5, 365	evlsaddval 40277	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))))
393	392	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
394	367, 379, 393	3eqtr4rd 2789	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
395		ovex 7308	. . . . . 6 ⊢ (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ V
396		fveq2 6774	. . . . . . . 8 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (𝑄‘𝑓) = (𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦)))
397	396	fveq1d 6776	. . . . . . 7 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
398	396	fveq1d 6776	. . . . . . . 8 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))
399	398	oveq2d 7291	. . . . . . 7 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
400	397, 399	eqeq12d 2754	. . . . . 6 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))))
401	395, 400	elab 3609	. . . . 5 ⊢ ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
402	394, 401	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
403	321, 402	sylan2b 594	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
404	1, 2, 3, 4, 5, 6, 7, 8, 13, 14, 15, 79, 300, 403	mhpind 40283	. 2 ⊢ (𝜑 → 𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
405		fveq2 6774	. . . . . 6 ⊢ (𝑓 = 𝑋 → (𝑄‘𝑓) = (𝑄‘𝑋))
406	405	fveq1d 6776	. . . . 5 ⊢ (𝑓 = 𝑋 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
407	405	fveq1d 6776	. . . . . 6 ⊢ (𝑓 = 𝑋 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑋)‘𝐴))
408	407	oveq2d 7291	. . . . 5 ⊢ (𝑓 = 𝑋 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
409	406, 408	eqeq12d 2754	. . . 4 ⊢ (𝑓 = 𝑋 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))))
410	409	elabg 3607	. . 3 ⊢ (𝑋 ∈ (𝐻‘𝑁) → (𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))))
411	15, 410	syl 17	. 2 ⊢ (𝜑 → (𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))))
412	404, 411	mpbid 231	1 ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {cab 2715  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∩ cin 3886   ⊆ wss 3887  ifcif 4459  {csn 4561   class class class wbr 5074   ↦ cmpt 5157   × cxp 5587  ^◡ccnv 5588   “ cima 5592  Fun wfun 6427   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∘_f cof 7531   supp csupp 7977   ↑_m cmap 8615  Fincfn 8733   finSupp cfsupp 9128  0cc0 10871  ℕcn 11973  ℕ₀cn0 12233  Basecbs 16912   ↾_s cress 16941  +_gcplusg 16962  ._rcmulr 16963  Scalarcsca 16965   ·_𝑠 cvsca 16966  0_gc0g 17150   Σ_g cgsu 17151   ↑_s cpws 17157  Mndcmnd 18385  SubMndcsubmnd 18429  ._gcmg 18700  CMndccmn 19386  mulGrpcmgp 19720  1_rcur 19737  Ringcrg 19783  CRingccrg 19784   RingHom crh 19956  SubRingcsubrg 20020  ℂ_fldccnfld 20597  AssAlgcasa 21057  algSccascl 21059   mPwSer cmps 21107   mPoly cmpl 21109   evalSub ces 21280   mHomP cmhp 21319

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-addf 10950  ax-mulf 10951

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-ofr 7534  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-oadd 8301  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-sup 9201  df-oi 9269  df-dju 9659  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-hom 16986  df-cco 16987  df-0g 17152  df-gsum 17153  df-prds 17158  df-pws 17160  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-mhm 18430  df-submnd 18431  df-grp 18580  df-minusg 18581  df-sbg 18582  df-mulg 18701  df-subg 18752  df-ghm 18832  df-cntz 18923  df-cmn 19388  df-abl 19389  df-mgp 19721  df-ur 19738  df-srg 19742  df-ring 19785  df-cring 19786  df-rnghom 19959  df-subrg 20022  df-lmod 20125  df-lss 20194  df-lsp 20234  df-cnfld 20598  df-assa 21060  df-asp 21061  df-ascl 21062  df-psr 21112  df-mvr 21113  df-mpl 21114  df-evls 21282  df-mhp 21323

This theorem is referenced by:  mhphf2  40286  mhphf3  40287