Theorem mhphf 40757

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 2736	. . 3 ⊢ (Base‘𝑈) = (Base‘𝑈)
3		eqid 2736	. . 3 ⊢ (0g‘𝑈) = (0g‘𝑈)
4		eqid 2736	. . 3 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈)
5		eqid 2736	. . 3 ⊢ (+g‘(𝐼 mPoly 𝑈)) = (+g‘(𝐼 mPoly 𝑈))
6		eqid 2736	. . 3 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
7		eqid 2736	. . 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 20225	. . . . 5 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
12	9, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ∈ Ring)
13	12	ringgrpd 19973	. . 3 ⊢ (𝜑 → 𝑈 ∈ Grp)
14		mhphf.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
15		mhphf.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
16		eqid 2736	. . . . . 6 ⊢ (algSc‘(𝐼 mPoly 𝑈)) = (algSc‘(𝐼 mPoly 𝑈))
17		eqid 2736	. . . . . 6 ⊢ (0g‘(𝐼 mPoly 𝑈)) = (0g‘(𝐼 mPoly 𝑈))
18		mhphf.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ CRing)
19	10	subrgcrng 20226	. . . . . . 7 ⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing)
20	18, 9, 19	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ CRing)
21	4, 16, 3, 17, 8, 20	mplascl0 40730	. . . . 5 ⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) = (0g‘(𝐼 mPoly 𝑈)))
22	4, 6, 3, 17, 8, 13	mpl0 21412	. . . . 5 ⊢ (𝜑 → (0g‘(𝐼 mPoly 𝑈)) = ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝑈)}))
23	21, 22	eqtr2d 2777	. . . 4 ⊢ (𝜑 → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝑈)}) = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))
24		mhphf.m	. . . . . . . . . 10 ⊢ · = (.r‘𝑆)
25	10, 24	ressmulr 17188	. . . . . . . . 9 ⊢ (𝑅 ∈ (SubRing‘𝑆) → · = (.r‘𝑈))
26	9, 25	syl 17	. . . . . . . 8 ⊢ (𝜑 → · = (.r‘𝑈))
27	26	oveqd 7374	. . . . . . 7 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · (0g‘𝑈)) = ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)))
28		eqid 2736	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
29	28	subrgsubm 20235	. . . . . . . . . . 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 18919	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)) ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ 𝑅) → (𝑁 ↑ 𝐿) ∈ 𝑅)
34	30, 14, 31, 33	syl3anc 1371	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝑅)
35	10	subrgbas 20231	. . . . . . . . . 10 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
36	9, 35	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 = (Base‘𝑈))
37	34, 36	eleqtrd 2840	. . . . . . . 8 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ (Base‘𝑈))
38		eqid 2736	. . . . . . . . 9 ⊢ (.r‘𝑈) = (.r‘𝑈)
39	2, 38, 3	ringrz 20012	. . . . . . . 8 ⊢ ((𝑈 ∈ Ring ∧ (𝑁 ↑ 𝐿) ∈ (Base‘𝑈)) → ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈))
40	12, 37, 39	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈))
41	27, 40	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · (0g‘𝑈)) = (0g‘𝑈))
42		mhphf.q	. . . . . . . . 9 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
43		mhphf.k	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑆)
44		eqid 2736	. . . . . . . . 9 ⊢ (Base‘(𝐼 mPoly 𝑈)) = (Base‘(𝐼 mPoly 𝑈))
45	2, 3	ring0cl 19990	. . . . . . . . . . 11 ⊢ (𝑈 ∈ Ring → (0g‘𝑈) ∈ (Base‘𝑈))
46	12, 45	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑈) ∈ (Base‘𝑈))
47	46, 36	eleqtrrd 2841	. . . . . . . . 9 ⊢ (𝜑 → (0g‘𝑈) ∈ 𝑅)
48		mhphf.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))
49	42, 4, 10, 43, 44, 16, 8, 18, 9, 47, 48	evlsscaval 40734	. . . . . . . 8 ⊢ (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴) = (0g‘𝑈)))
50	49	simprd 496	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴) = (0g‘𝑈))
51	50	oveq2d 7373	. . . . . 6 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)) = ((𝑁 ↑ 𝐿) · (0g‘𝑈)))
52	43	fvexi 6856	. . . . . . . . . 10 ⊢ 𝐾 ∈ V
53	52	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ V)
54	18	crngringd 19977	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Ring)
55	43, 24	ringcl 19981	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
56	54, 55	syl3an1 1163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
57	56	3expb 1120	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
58	43	subrgss 20223	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾)
59	9, 58	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⊆ 𝐾)
60	59, 31	sseldd 3945	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ 𝐾)
61		fconst6g 6731	. . . . . . . . . . 11 ⊢ (𝐿 ∈ 𝐾 → (𝐼 × {𝐿}):𝐼⟶𝐾)
62	60, 61	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝐾)
63		elmapi 8787	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐾 ↑m 𝐼) → 𝐴:𝐼⟶𝐾)
64	48, 63	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:𝐼⟶𝐾)
65		inidm 4178	. . . . . . . . . 10 ⊢ (𝐼 ∩ 𝐼) = 𝐼
66	57, 62, 64, 8, 8, 65	off 7635	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾)
67	53, 8, 66	elmapdd 40664	. . . . . . . 8 ⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼))
68	42, 4, 10, 43, 44, 16, 8, 18, 9, 47, 67	evlsscaval 40734	. . . . . . 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 2787	. . . . 5 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)))
71		fvex 6855	. . . . . 6 ⊢ ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ V
72		fveq2 6842	. . . . . . . 8 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → (𝑄‘𝑓) = (𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈))))
73	72	fveq1d 6844	. . . . . . 7 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
74	72	fveq1d 6844	. . . . . . . 8 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))
75	74	oveq2d 7373	. . . . . . 7 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)))
76	73, 75	eqeq12d 2752	. . . . . 6 ⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))))
77	71, 76	elab 3630	. . . . 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 2838	. . 3 ⊢ (𝜑 → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝑈)}) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
80	4	mplassa 21427	. . . . . . . . 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 21417	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 = (Scalar‘(𝐼 mPoly 𝑈)))
84	83	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑈) = (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
85	84	eleq2d 2823	. . . . . . . . 9 ⊢ (𝜑 → (𝑏 ∈ (Base‘𝑈) ↔ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈)))))
86	85	biimpa 477	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
87	86	adantrl 714	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
88		fvexd 6857	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑈) ∈ V)
89		ovex 7390	. . . . . . . . . . . . 13 ⊢ (ℕ0 ↑m 𝐼) ∈ V
90	89	rabex 5289	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V)
92		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑈) = (1r‘𝑈)
93	2, 92	ringidcl 19989	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ Ring → (1r‘𝑈) ∈ (Base‘𝑈))
94	12, 93	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝑈) ∈ (Base‘𝑈))
95	94, 46	ifcld 4532	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ (Base‘𝑈))
96	95	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ (Base‘𝑈))
97	96	fmpttd 7063	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))):{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑈))
98	88, 91, 97	elmapdd 40664	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ ((Base‘𝑈) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}))
99		eqid 2736	. . . . . . . . . . 11 ⊢ (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
100		eqid 2736	. . . . . . . . . . 11 ⊢ (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
101	99, 2, 6, 100, 8	psrbas 21346	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}))
102	98, 101	eleqtrrd 2841	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)))
103	90	mptex 7173	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ V
104	103	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ V)
105		fvexd 6857	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑈) ∈ V)
106		funmpt 6539	. . . . . . . . . . 11 ⊢ Fun (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
107	106	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))
108		snfi 8988	. . . . . . . . . . . 12 ⊢ {𝑎} ∈ Fin
109	108	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎} ∈ Fin)
110		eldifsnneq 4751	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎}) → ¬ 𝑤 = 𝑎)
111	110	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎})) → ¬ 𝑤 = 𝑎)
112	111	iffalsed 4497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎})) → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) = (0g‘𝑈))
113	112, 91	suppss2 8131	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) supp (0g‘𝑈)) ⊆ {𝑎})
114	109, 113	ssfid 9211	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) supp (0g‘𝑈)) ∈ Fin)
115	104, 105, 107, 114	isfsuppd 40665	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) finSupp (0g‘𝑈))
116	4, 99, 100, 3, 44	mplelbas 21399	. . . . . . . . 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 2736	. . . . . . . 8 ⊢ (Scalar‘(𝐼 mPoly 𝑈)) = (Scalar‘(𝐼 mPoly 𝑈))
120		eqid 2736	. . . . . . . 8 ⊢ (Base‘(Scalar‘(𝐼 mPoly 𝑈))) = (Base‘(Scalar‘(𝐼 mPoly 𝑈)))
121		eqid 2736	. . . . . . . 8 ⊢ (.r‘(𝐼 mPoly 𝑈)) = (.r‘(𝐼 mPoly 𝑈))
122		eqid 2736	. . . . . . . 8 ⊢ ( ·𝑠 ‘(𝐼 mPoly 𝑈)) = ( ·𝑠 ‘(𝐼 mPoly 𝑈))
123	16, 119, 120, 44, 121, 122	asclmul1 21289	. . . . . . 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 1371	. . . . . 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 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘𝑈))
126	4, 122, 2, 44, 38, 6, 125, 118	mplvsca 21419	. . . . . 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 2776	. . . . 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 3449	. . . . . . 7 ⊢ 𝑏 ∈ V
129		fnconstg 6730	. . . . . . 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 6855	. . . . . . . . 9 ⊢ (1r‘𝑈) ∈ V
132		fvex 6855	. . . . . . . . 9 ⊢ (0g‘𝑈) ∈ V
133	131, 132	ifex 4536	. . . . . . . 8 ⊢ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ V
134		eqid 2736	. . . . . . . 8 ⊢ (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = (𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
135	133, 134	fnmpti 6644	. . . . . . 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 4178	. . . . . 6 ⊢ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∩ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
139	128	fvconst2 7153	. . . . . . 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 4509	. . . . . . . 8 ⊢ (𝑤 = 𝑠 → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))
143	131, 132	ifex 4536	. . . . . . . 8 ⊢ if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ V
144	142, 134, 143	fvmpt 6948	. . . . . . 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 7626	. . . . 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 7455	. . . . . . 7 ⊢ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = if(𝑠 = 𝑎, (𝑏(.r‘𝑈)(1r‘𝑈)), (𝑏(.r‘𝑈)(0g‘𝑈)))
148	12	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑈 ∈ Ring)
149		simplrr 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑏 ∈ (Base‘𝑈))
150	2, 38, 92, 148, 149	ringridmd 40692	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)(1r‘𝑈)) = 𝑏)
151	2, 38, 3	ringrz 20012	. . . . . . . . 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 4507	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → if(𝑠 = 𝑎, (𝑏(.r‘𝑈)(1r‘𝑈)), (𝑏(.r‘𝑈)(0g‘𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g‘𝑈)))
154	147, 153	eqtrid 2788	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g‘𝑈)))
155	154	mpteq2dva 5205	. . . . 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 2780	. . . 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 21473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (algSc‘(𝐼 mPoly 𝑈)):(Base‘𝑈)⟶(Base‘(𝐼 mPoly 𝑈)))
163	162, 125	ffvelcdmd 7036	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)))
164		eqidd 2737	. . . . . . . . 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 3639	. . . . . . . . . 10 ⊢ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
167	166	ad2antrl 726	. . . . . . . . 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 40736	. . . . . . . 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 40739	. . . . . . 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, 43	mgpbas 19902	. . . . . . . . . . . 12 ⊢ 𝐾 = (Base‘(mulGrp‘𝑆))
172	28	ringmgp 19970	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
173	54, 172	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
174	171, 32, 173, 14, 60	mulgnn0cld 18897	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝐾)
175	174	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑁 ↑ 𝐿) ∈ 𝐾)
176	36, 59	eqsstrrd 3983	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾)
177	176	sselda 3944	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ 𝐾)
178	177	adantrl 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ 𝐾)
179	43, 24	crngcom 19982	. . . . . . . . . 10 ⊢ ((𝑆 ∈ CRing ∧ (𝑁 ↑ 𝐿) ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → ((𝑁 ↑ 𝐿) · 𝑏) = (𝑏 · (𝑁 ↑ 𝐿)))
180	158, 175, 178, 179	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · 𝑏) = (𝑏 · (𝑁 ↑ 𝐿)))
181	180	oveq1d 7372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 ↑ 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑏 · (𝑁 ↑ 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
182	158	crngringd 19977	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ Ring)
183		eqid 2736	. . . . . . . . . . 11 ⊢ (1r‘𝑆) = (1r‘𝑆)
184	28, 183	ringidval 19915	. . . . . . . . . 10 ⊢ (1r‘𝑆) = (0g‘(mulGrp‘𝑆))
185	28	crngmgp 19972	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CRing → (mulGrp‘𝑆) ∈ CMnd)
186	18, 185	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ CMnd)
187	186	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (mulGrp‘𝑆) ∈ CMnd)
188	173	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd)
189		elrabi 3639	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑎 ∈ (ℕ0 ↑m 𝐼))
190		elmapi 8787	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (ℕ0 ↑m 𝐼) → 𝑎:𝐼⟶ℕ0)
191	166, 189, 190	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎:𝐼⟶ℕ0)
192	191	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝑎:𝐼⟶ℕ0)
193	192	adantrr 715	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎:𝐼⟶ℕ0)
194	193	ffvelcdmda 7035	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈ ℕ0)
195	64	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐴:𝐼⟶𝐾)
196		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
197	195, 196	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾)
198	171, 32, 188, 194, 197	mulgnn0cld 18897	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾)
199	198	fmpttd 7063	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))):𝐼⟶𝐾)
200	6	psrbagfsupp 21322	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑎 finSupp 0)
201	200	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑎 finSupp 0)
202	201	fsuppimpd 9312	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑎 supp 0) ∈ Fin)
203	166, 202	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ∈ Fin)
204	203	adantrr 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ∈ Fin)
205	193	feqmptd 6910	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)))
206	205	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) = ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0))
207		ssidd 3967	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
208	206, 207	eqsstrrd 3983	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0) ⊆ (𝑎 supp 0))
209	171, 184, 32	mulg0 18879	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐾 → (0 ↑ 𝑘) = (1r‘𝑆))
210	209	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆))
211		c0ex 11149	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
212	211	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 0 ∈ V)
213	208, 210, 194, 197, 212	suppssov1 8129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ⊆ (𝑎 supp 0))
214	204, 213	ssfid 9211	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ∈ Fin)
215	171, 184, 187, 157, 199, 214	gsumcl2 19691	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾)
216	43, 24, 182, 175, 178, 215	ringassd 40690	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 ↑ 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
217	43, 24, 182, 178, 175, 215	ringassd 40690	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑏 · (𝑁 ↑ 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = (𝑏 · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
218	181, 216, 217	3eqtr3d 2784	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) = (𝑏 · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
219	48	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 ∈ (𝐾 ↑m 𝐼))
220	36	eleq2d 2823	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑏 ∈ 𝑅 ↔ 𝑏 ∈ (Base‘𝑈)))
221	220	biimpar 478	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ 𝑅)
222	221	adantrl 714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ 𝑅)
223	42, 4, 10, 43, 44, 16, 157, 158, 159, 222, 219	evlsscaval 40734	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘𝐴) = 𝑏))
224	42, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 219, 167	evlsbagval 40736	. . . . . . . . . 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 (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
225	42, 4, 10, 43, 44, 157, 158, 159, 219, 223, 224, 121, 24	evlsmulval 40739	. . . . . . . . 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 (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
226	225	simprd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴) = (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
227	226	oveq2d 7373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)) = ((𝑁 ↑ 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
228	42, 4, 10, 43, 44, 16, 157, 158, 159, 222, 160	evlsscaval 40734	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏))
229	228	simprd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏)
230		fconst6g 6731	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ 𝑅 → (𝐼 × {𝐿}):𝐼⟶𝑅)
231	31, 230	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝑅)
232	231	ffnd 6669	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 × {𝐿}) Fn 𝐼)
233	232	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 × {𝐿}) Fn 𝐼)
234	64	ffnd 6669	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 Fn 𝐼)
235	234	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 Fn 𝐼)
236	31	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝑅)
237		fvconst2g 7151	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ 𝑅 ∧ 𝑣 ∈ 𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
238	236, 196, 237	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
239		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) = (𝐴‘𝑣))
240	233, 235, 157, 157, 65, 238, 239	ofval 7628	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣) = (𝐿 · (𝐴‘𝑣)))
241	240	oveq2d 7373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))))
242	186	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ CMnd)
243	60	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝐾)
244	28, 24	mgpplusg 19900	. . . . . . . . . . . . . 14 ⊢ · = (+g‘(mulGrp‘𝑆))
245	171, 32, 244	mulgnn0di 19604	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘𝑆) ∈ CMnd ∧ ((𝑎‘𝑣) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ (𝐴‘𝑣) ∈ 𝐾)) → ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
246	242, 194, 243, 197, 245	syl13anc 1372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
247	241, 246	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
248	247	mpteq2dva 5205	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))
249	248	oveq2d 7373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
250	186	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd)
251	8	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝐼 ∈ 𝑉)
252	173	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd)
253	192	ffvelcdmda 7035	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈ ℕ0)
254	60	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝐾)
255	171, 32, 252, 253, 254	mulgnn0cld 18897	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ 𝐿) ∈ 𝐾)
256	64	ffvelcdmda 7035	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾)
257	256	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾)
258	171, 32, 252, 253, 257	mulgnn0cld 18897	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾)
259		eqidd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) = (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)))
260		eqidd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) = (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
261	251	mptexd 7174	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) ∈ V)
262		fvexd 6857	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (1r‘𝑆) ∈ V)
263		funmpt 6539	. . . . . . . . . . . . . 14 ⊢ Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))
264	263	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)))
265	192	feqmptd 6910	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)))
266	265	oveq1d 7372	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) = ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0))
267		ssidd 3967	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
268	266, 267	eqsstrrd 3983	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0) ⊆ (𝑎 supp 0))
269	209	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆))
270	211	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 0 ∈ V)
271	268, 269, 253, 254, 270	suppssov1 8129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) supp (1r‘𝑆)) ⊆ (𝑎 supp 0))
272	203, 271	ssfid 9211	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) supp (1r‘𝑆)) ∈ Fin)
273	261, 262, 264, 272	isfsuppd 40665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) finSupp (1r‘𝑆))
274	251	mptexd 7174	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) ∈ V)
275		funmpt 6539	. . . . . . . . . . . . . 14 ⊢ Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))
276	275	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))
277	268, 269, 253, 257, 270	suppssov1 8129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ⊆ (𝑎 supp 0))
278	203, 277	ssfid 9211	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ∈ Fin)
279	274, 262, 276, 278	isfsuppd 40665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) finSupp (1r‘𝑆))
280	171, 184, 244, 250, 251, 255, 258, 259, 260, 273, 279	gsummptfsadd 19701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = (((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
281	6, 7, 171, 32, 8, 173, 60, 14	mhphflem 40756	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) = (𝑁 ↑ 𝐿))
282	281	oveq1d 7372	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
283	280, 282	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
284	283	adantrr 715	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
285	249, 284	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))
286	229, 285	oveq12d 7375	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = (𝑏 · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))))
287	218, 227, 286	3eqtr4rd 2787	. . . . . 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‘𝑈)))))‘𝐴)))
288	170, 287	eqtrd 2776	. . . . 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‘𝑈)))))‘𝐴)))
289		ovex 7390	. . . . . 6 ⊢ (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ V
290		fveq2 6842	. . . . . . . 8 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → (𝑄‘𝑓) = (𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))))
291	290	fveq1d 6844	. . . . . . 7 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
292	290	fveq1d 6844	. . . . . . . 8 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))
293	292	oveq2d 7373	. . . . . . 7 ⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)))
294	291, 293	eqeq12d 2752	. . . . . 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‘𝑈)))))‘𝐴))))
295	289, 294	elab 3630	. . . . 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‘𝑈)))))‘𝐴)))
296	288, 295	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
297	156, 296	eqeltrrd 2839	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
298		elin 3926	. . . . . 6 ⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))
299		vex 3449	. . . . . . . 8 ⊢ 𝑥 ∈ V
300		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑓 = 𝑥 → (𝑄‘𝑓) = (𝑄‘𝑥))
301	300	fveq1d 6844	. . . . . . . . 9 ⊢ (𝑓 = 𝑥 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
302	300	fveq1d 6844	. . . . . . . . . 10 ⊢ (𝑓 = 𝑥 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑥)‘𝐴))
303	302	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑓 = 𝑥 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))
304	301, 303	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑓 = 𝑥 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
305	299, 304	elab 3630	. . . . . . 7 ⊢ (𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))
306	305	anbi2i 623	. . . . . 6 ⊢ ((𝑥 ∈ (𝐻‘𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
307	298, 306	bitri 274	. . . . 5 ⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
308		elin 3926	. . . . . 6 ⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))
309		vex 3449	. . . . . . . 8 ⊢ 𝑦 ∈ V
310		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑓 = 𝑦 → (𝑄‘𝑓) = (𝑄‘𝑦))
311	310	fveq1d 6844	. . . . . . . . 9 ⊢ (𝑓 = 𝑦 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
312	310	fveq1d 6844	. . . . . . . . . 10 ⊢ (𝑓 = 𝑦 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑦)‘𝐴))
313	312	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑓 = 𝑦 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))
314	311, 313	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑓 = 𝑦 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
315	309, 314	elab 3630	. . . . . . 7 ⊢ (𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))
316	315	anbi2i 623	. . . . . 6 ⊢ ((𝑦 ∈ (𝐻‘𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
317	308, 316	bitri 274	. . . . 5 ⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
318	307, 317	anbi12i 627	. . . 4 ⊢ ((𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})) ↔ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))))
319	54	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑆 ∈ Ring)
320	174	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑁 ↑ 𝐿) ∈ 𝐾)
321		eqid 2736	. . . . . . . . 9 ⊢ (𝑆 ↑s (Base‘(𝑆 ↑s 𝐼))) = (𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))
322		eqid 2736	. . . . . . . . 9 ⊢ (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))) = (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼))))
323	18	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑆 ∈ CRing)
324		fvexd 6857	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (Base‘(𝑆 ↑s 𝐼)) ∈ V)
325		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ↑s (𝐾 ↑m 𝐼)) = (𝑆 ↑s (𝐾 ↑m 𝐼))
326	42, 4, 10, 325, 43	evlsrhm 21498	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))))
327	8, 18, 9, 326	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))))
328		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))
329	44, 328	rhmf 20158	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
330	327, 329	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
331	330	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
332	8	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝐼 ∈ 𝑉)
333	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑈 ∈ Ring)
334	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑁 ∈ ℕ0)
335		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑥 ∈ (𝐻‘𝑁))
336	1, 4, 44, 332, 333, 334, 335	mhpmpl 21534	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
337	336	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
338	337	adantrr 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
339	331, 338	ffvelcdmd 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
340		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ↑s 𝐼) = (𝑆 ↑s 𝐼)
341	340, 43	pwsbas 17369	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ CRing ∧ 𝐼 ∈ 𝑉) → (𝐾 ↑m 𝐼) = (Base‘(𝑆 ↑s 𝐼)))
342	18, 8, 341	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ↑m 𝐼) = (Base‘(𝑆 ↑s 𝐼)))
343	342	oveq2d 7373	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ↑s (𝐾 ↑m 𝐼)) = (𝑆 ↑s (Base‘(𝑆 ↑s 𝐼))))
344	343	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
345	344	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
346	339, 345	eleqtrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥) ∈ (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
347	321, 43, 322, 323, 324, 346	pwselbas 17371	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥):(Base‘(𝑆 ↑s 𝐼))⟶𝐾)
348	48, 342	eleqtrd 2840	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Base‘(𝑆 ↑s 𝐼)))
349	348	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴 ∈ (Base‘(𝑆 ↑s 𝐼)))
350	347, 349	ffvelcdmd 7036	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘𝑥)‘𝐴) ∈ 𝐾)
351	8	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝐼 ∈ 𝑉)
352	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑈 ∈ Ring)
353	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑁 ∈ ℕ0)
354		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑦 ∈ (𝐻‘𝑁))
355	1, 4, 44, 351, 352, 353, 354	mhpmpl 21534	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
356	355	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
357	356	adantrl 714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
358	331, 357	ffvelcdmd 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))))
359	358, 345	eleqtrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦) ∈ (Base‘(𝑆 ↑s (Base‘(𝑆 ↑s 𝐼)))))
360	321, 43, 322, 323, 324, 359	pwselbas 17371	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦):(Base‘(𝑆 ↑s 𝐼))⟶𝐾)
361	360, 349	ffvelcdmd 7036	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘𝑦)‘𝐴) ∈ 𝐾)
362		eqid 2736	. . . . . . . 8 ⊢ (+g‘𝑆) = (+g‘𝑆)
363	43, 362, 24	ringdi 19987	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ ((𝑁 ↑ 𝐿) ∈ 𝐾 ∧ ((𝑄‘𝑥)‘𝐴) ∈ 𝐾 ∧ ((𝑄‘𝑦)‘𝐴) ∈ 𝐾)) → ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
364	319, 320, 350, 361, 363	syl13anc 1372	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
365	8	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐼 ∈ 𝑉)
366	9	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑅 ∈ (SubRing‘𝑆))
367	48	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴 ∈ (𝐾 ↑m 𝐼))
368		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) → ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴))
369	336, 368	anim12dan 619	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴)))
370	369	adantrr 715	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴)))
371		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) → ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴))
372	355, 371	anim12dan 619	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴)))
373	372	adantrl 714	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴)))
374	42, 4, 10, 43, 44, 365, 323, 366, 367, 370, 373, 5, 362	evlsaddval 40738	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))))
375	374	simprd 496	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴)))
376	375	oveq2d 7373	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)) = ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))))
377	52	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐾 ∈ V)
378	57	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
379	62	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝐼 × {𝐿}):𝐼⟶𝐾)
380	64	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴:𝐼⟶𝐾)
381	378, 379, 380, 365, 365, 65	off 7635	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾)
382	377, 365, 381	elmapdd 40664	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼))
383		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) → ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))
384	336, 383	anim12dan 619	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
385	384	adantrr 715	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))))
386		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) → ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))
387	355, 386	anim12dan 619	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
388	387	adantrl 714	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
389	42, 4, 10, 43, 44, 365, 323, 366, 382, 385, 388, 5, 362	evlsaddval 40738	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))))
390	389	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))
391	364, 376, 390	3eqtr4rd 2787	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
392		ovex 7390	. . . . . 6 ⊢ (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ V
393		fveq2 6842	. . . . . . . 8 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (𝑄‘𝑓) = (𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦)))
394	393	fveq1d 6844	. . . . . . 7 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
395	393	fveq1d 6844	. . . . . . . 8 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))
396	395	oveq2d 7373	. . . . . . 7 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
397	394, 396	eqeq12d 2752	. . . . . 6 ⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))))
398	392, 397	elab 3630	. . . . 5 ⊢ ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
399	391, 398	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
400	318, 399	sylan2b 594	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
401	1, 2, 3, 4, 5, 6, 7, 8, 13, 14, 15, 79, 297, 400	mhpind 40755	. 2 ⊢ (𝜑 → 𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})
402		fveq2 6842	. . . . . 6 ⊢ (𝑓 = 𝑋 → (𝑄‘𝑓) = (𝑄‘𝑋))
403	402	fveq1d 6844	. . . . 5 ⊢ (𝑓 = 𝑋 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
404	402	fveq1d 6844	. . . . . 6 ⊢ (𝑓 = 𝑋 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑋)‘𝐴))
405	404	oveq2d 7373	. . . . 5 ⊢ (𝑓 = 𝑋 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
406	403, 405	eqeq12d 2752	. . . 4 ⊢ (𝑓 = 𝑋 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))))
407	406	elabg 3628	. . 3 ⊢ (𝑋 ∈ (𝐻‘𝑁) → (𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))))
408	15, 407	syl 17	. 2 ⊢ (𝜑 → (𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))))
409	401, 408	mpbid 231	1 ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2713  {crab 3407  Vcvv 3445   ∖ cdif 3907   ∩ cin 3909   ⊆ wss 3910  ifcif 4486  {csn 4586   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  ^◡ccnv 5632   “ cima 5636  Fun wfun 6490   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ∘_f cof 7615   supp csupp 8092   ↑_m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  0cc0 11051  ℕcn 12153  ℕ₀cn0 12413  Basecbs 17083   ↾_s cress 17112  +_gcplusg 17133  ._rcmulr 17134  Scalarcsca 17136   ·_𝑠 cvsca 17137  0_gc0g 17321   Σ_g cgsu 17322   ↑_s cpws 17328  Mndcmnd 18556  SubMndcsubmnd 18600  ._gcmg 18872  CMndccmn 19562  mulGrpcmgp 19896  1_rcur 19913  Ringcrg 19964  CRingccrg 19965   RingHom crh 20143  SubRingcsubrg 20218  ℂ_fldccnfld 20796  AssAlgcasa 21256  algSccascl 21258   mPwSer cmps 21306   mPoly cmpl 21308   evalSub ces 21480   mHomP cmhp 21519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-addf 11130  ax-mulf 11131

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-srg 19918  df-ring 19966  df-cring 19967  df-rnghom 20146  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-cnfld 20797  df-assa 21259  df-asp 21260  df-ascl 21261  df-psr 21311  df-mvr 21312  df-mpl 21313  df-evls 21482  df-mhp 21523

This theorem is referenced by:  mhphf2  40758  mhphf3  40759