mhphf

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 ( QX ) which corresponds to X ). (Contributed by SN, 28-Jul-2024)

	Ref	Expression
Hypotheses	mhphf.q	$⊢ Q = (I evalSub S) (R)$
	mhphf.h	$⊢ H = I mHomP U$
	mhphf.u	$⊢ U = S ↾_{𝑠} R$
	mhphf.k	$⊢ K = {Base}_{S}$
	mhphf.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	mhphf.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
	mhphf.i	$⊢ φ \to I \in V$
	mhphf.s	$⊢ φ \to S \in CRing$
	mhphf.r	$⊢ φ \to R \in SubRing (S)$
	mhphf.l	$⊢ φ \to L \in R$
	mhphf.n	$⊢ φ \to N \in ℕ_{0}$
	mhphf.x	$⊢ φ \to X \in H (N)$
	mhphf.a	$⊢ φ \to A \in (K^{I})$
Assertion	mhphf	$⊢ φ \to Q (X) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A)$

Proof

Step	Hyp	Ref	Expression
1		mhphf.q	$⊢ Q = (I evalSub S) (R)$
2		mhphf.h	$⊢ H = I mHomP U$
3		mhphf.u	$⊢ U = S ↾_{𝑠} R$
4		mhphf.k	$⊢ K = {Base}_{S}$
5		mhphf.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
6		mhphf.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
7		mhphf.i	$⊢ φ \to I \in V$
8		mhphf.s	$⊢ φ \to S \in CRing$
9		mhphf.r	$⊢ φ \to R \in SubRing (S)$
10		mhphf.l	$⊢ φ \to L \in R$
11		mhphf.n	$⊢ φ \to N \in ℕ_{0}$
12		mhphf.x	$⊢ φ \to X \in H (N)$
13		mhphf.a	$⊢ φ \to A \in (K^{I})$
14		eqid	$⊢ {Base}_{U} = {Base}_{U}$
15		eqid	$⊢ 0_{U} = 0_{U}$
16		eqid	$⊢ I mPoly U = I mPoly U$
17		eqid	$⊢ +_{(I mPoly U)} = +_{(I mPoly U)}$
18		eqid	$⊢ \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
19		eqid	$⊢ \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} = \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
20	3	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
21	9 20	syl	$⊢ φ \to U \in Ring$
22	21	ringgrpd	$⊢ φ \to U \in Grp$
23	16 7 21	mplsca	$⊢ φ \to U = Scalar (I mPoly U)$
24	23	fveq2d	$⊢ φ \to 0_{U} = 0_{Scalar (I mPoly U)}$
25	24	fveq2d	$⊢ φ \to algSc (I mPoly U) (0_{U}) = algSc (I mPoly U) (0_{Scalar (I mPoly U)})$
26		eqid	$⊢ algSc (I mPoly U) = algSc (I mPoly U)$
27		eqid	$⊢ Scalar (I mPoly U) = Scalar (I mPoly U)$
28	16	mpllmod	$⊢ (I \in V \land U \in Ring) \to I mPoly U \in LMod$
29	7 21 28	syl2anc	$⊢ φ \to I mPoly U \in LMod$
30	16	mplring	$⊢ (I \in V \land U \in Ring) \to I mPoly U \in Ring$
31	7 21 30	syl2anc	$⊢ φ \to I mPoly U \in Ring$
32	26 27 29 31	ascl0	$⊢ φ \to algSc (I mPoly U) (0_{Scalar (I mPoly U)}) = 0_{(I mPoly U)}$
33		eqid	$⊢ 0_{(I mPoly U)} = 0_{(I mPoly U)}$
34	16 18 15 33 7 22	mpl0	$⊢ φ \to 0_{(I mPoly U)} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{U}\}$
35	25 32 34	3eqtrrd	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{U}\} = algSc (I mPoly U) (0_{U})$
36	3 5	ressmulr	$⊢ R \in SubRing (S) \to \underset{˙}{\cdot} = \cdot_{U}$
37	9 36	syl	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{U}$
38	37	oveqd	$⊢ φ \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} 0_{U} = (N \underset{˙}{\times} L) \cdot_{U} 0_{U}$
39		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
40	39	subrgsubm	$⊢ R \in SubRing (S) \to R \in SubMnd ({mulGrp}_{S})$
41	9 40	syl	$⊢ φ \to R \in SubMnd ({mulGrp}_{S})$
42	6	submmulgcl	$⊢ (R \in SubMnd ({mulGrp}_{S}) \land N \in ℕ_{0} \land L \in R) \to N \underset{˙}{\times} L \in R$
43	41 11 10 42	syl3anc	$⊢ φ \to N \underset{˙}{\times} L \in R$
44	3	subrgbas	$⊢ R \in SubRing (S) \to R = {Base}_{U}$
45	9 44	syl	$⊢ φ \to R = {Base}_{U}$
46	43 45	eleqtrd	$⊢ φ \to N \underset{˙}{\times} L \in {Base}_{U}$
47		eqid	$⊢ \cdot_{U} = \cdot_{U}$
48	14 47 15	ringrz	$⊢ (U \in Ring \land N \underset{˙}{\times} L \in {Base}_{U}) \to (N \underset{˙}{\times} L) \cdot_{U} 0_{U} = 0_{U}$
49	21 46 48	syl2anc	$⊢ φ \to (N \underset{˙}{\times} L) \cdot_{U} 0_{U} = 0_{U}$
50	38 49	eqtrd	$⊢ φ \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} 0_{U} = 0_{U}$
51		eqid	$⊢ {Base}_{(I mPoly U)} = {Base}_{(I mPoly U)}$
52	14 15	ring0cl	$⊢ U \in Ring \to 0_{U} \in {Base}_{U}$
53	21 52	syl	$⊢ φ \to 0_{U} \in {Base}_{U}$
54	53 45	eleqtrrd	$⊢ φ \to 0_{U} \in R$
55	1 16 3 4 51 26 7 8 9 54 13	evlsscaval	$⊢ φ \to (algSc (I mPoly U) (0_{U}) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (0_{U})) (A) = 0_{U})$
56	55	simprd	$⊢ φ \to Q (algSc (I mPoly U) (0_{U})) (A) = 0_{U}$
57	56	oveq2d	$⊢ φ \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (0_{U})) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} 0_{U}$
58	4	fvexi	$⊢ K \in V$
59	58	a1i	$⊢ φ \to K \in V$
60	8	crngringd	$⊢ φ \to S \in Ring$
61	4 5	ringcl	$⊢ (S \in Ring \land j \in K \land k \in K) \to j \underset{˙}{\cdot} k \in K$
62	60 61	syl3an1	$⊢ (φ \land j \in K \land k \in K) \to j \underset{˙}{\cdot} k \in K$
63	62	3expb	$⊢ (φ \land (j \in K \land k \in K)) \to j \underset{˙}{\cdot} k \in K$
64	4	subrgss	$⊢ R \in SubRing (S) \to R \subseteq K$
65	9 64	syl	$⊢ φ \to R \subseteq K$
66	65 10	sseldd	$⊢ φ \to L \in K$
67		fconst6g	$⊢ L \in K \to (I \times \{L\}) : I ⟶ K$
68	66 67	syl	$⊢ φ \to (I \times \{L\}) : I ⟶ K$
69		elmapi	$⊢ A \in (K^{I}) \to A : I ⟶ K$
70	13 69	syl	$⊢ φ \to A : I ⟶ K$
71		inidm	$⊢ I \cap I = I$
72	63 68 70 7 7 71	off	$⊢ φ \to ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) : I ⟶ K$
73	59 7 72	elmapdd	$⊢ φ \to (I \times \{L\}) {\underset{˙}{\cdot}}_{f} A \in (K^{I})$
74	1 16 3 4 51 26 7 8 9 54 73	evlsscaval	$⊢ φ \to (algSc (I mPoly U) (0_{U}) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (0_{U})) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = 0_{U})$
75	74	simprd	$⊢ φ \to Q (algSc (I mPoly U) (0_{U})) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = 0_{U}$
76	50 57 75	3eqtr4rd	$⊢ φ \to Q (algSc (I mPoly U) (0_{U})) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (0_{U})) (A)$
77		fvex	$⊢ algSc (I mPoly U) (0_{U}) \in V$
78		fveq2	$⊢ f = algSc (I mPoly U) (0_{U}) \to Q (f) = Q (algSc (I mPoly U) (0_{U}))$
79	78	fveq1d	$⊢ f = algSc (I mPoly U) (0_{U}) \to Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (algSc (I mPoly U) (0_{U})) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
80	78	fveq1d	$⊢ f = algSc (I mPoly U) (0_{U}) \to Q (f) (A) = Q (algSc (I mPoly U) (0_{U})) (A)$
81	80	oveq2d	$⊢ f = algSc (I mPoly U) (0_{U}) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (0_{U})) (A)$
82	79 81	eqeq12d	$⊢ f = algSc (I mPoly U) (0_{U}) \to (Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) \leftrightarrow Q (algSc (I mPoly U) (0_{U})) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (0_{U})) (A))$
83	77 82	elab	$⊢ algSc (I mPoly U) (0_{U}) \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (algSc (I mPoly U) (0_{U})) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (0_{U})) (A)$
84	76 83	sylibr	$⊢ φ \to algSc (I mPoly U) (0_{U}) \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
85	35 84	eqeltrd	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{U}\} \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
86	3	subrgcrng	$⊢ (S \in CRing \land R \in SubRing (S)) \to U \in CRing$
87	8 9 86	syl2anc	$⊢ φ \to U \in CRing$
88	16	mplassa	$⊢ (I \in V \land U \in CRing) \to I mPoly U \in AssAlg$
89	7 87 88	syl2anc	$⊢ φ \to I mPoly U \in AssAlg$
90	89	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to I mPoly U \in AssAlg$
91	23	fveq2d	$⊢ φ \to {Base}_{U} = {Base}_{Scalar (I mPoly U)}$
92	91	eleq2d	$⊢ φ \to (b \in {Base}_{U} \leftrightarrow b \in {Base}_{Scalar (I mPoly U)})$
93	92	biimpa	$⊢ (φ \land b \in {Base}_{U}) \to b \in {Base}_{Scalar (I mPoly U)}$
94	93	adantrl	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to b \in {Base}_{Scalar (I mPoly U)}$
95		fvexd	$⊢ φ \to {Base}_{U} \in V$
96		ovex	$⊢ {ℕ_{0}}^{I} \in V$
97	96	rabex	$⊢ \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \in V$
98	97	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \in V$
99		eqid	$⊢ 1_{U} = 1_{U}$
100	14 99	ringidcl	$⊢ U \in Ring \to 1_{U} \in {Base}_{U}$
101	21 100	syl	$⊢ φ \to 1_{U} \in {Base}_{U}$
102	101 53	ifcld	$⊢ φ \to if (w = a, 1_{U}, 0_{U}) \in {Base}_{U}$
103	102	adantr	$⊢ (φ \land w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to if (w = a, 1_{U}, 0_{U}) \in {Base}_{U}$
104	103	fmpttd	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) : \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟶ {Base}_{U}$
105	95 98 104	elmapdd	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in ({Base}_{U}^{\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}})$
106		eqid	$⊢ I mPwSer U = I mPwSer U$
107		eqid	$⊢ {Base}_{(I mPwSer U)} = {Base}_{(I mPwSer U)}$
108	106 14 18 107 7	psrbas	$⊢ φ \to {Base}_{(I mPwSer U)} = {Base}_{U}^{\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}}$
109	105 108	eleqtrrd	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPwSer U)}$
110	97	mptex	$⊢ (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in V$
111	110	a1i	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in V$
112		fvexd	$⊢ φ \to 0_{U} \in V$
113		funmpt	$⊢ Fun (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
114	113	a1i	$⊢ φ \to Fun (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
115		snfi	$⊢ \{a\} \in Fin$
116	115	a1i	$⊢ φ \to \{a\} \in Fin$
117		eldifsnneq	$⊢ w \in (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ∖ \{a\}) \to \neg w = a$
118	117	adantl	$⊢ (φ \land w \in (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ∖ \{a\})) \to \neg w = a$
119	118	iffalsed	$⊢ (φ \land w \in (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ∖ \{a\})) \to if (w = a, 1_{U}, 0_{U}) = 0_{U}$
120	119 98	suppss2	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) supp 0_{U} \subseteq \{a\}$
121	116 120	ssfid	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) supp 0_{U} \in Fin$
122	111 112 114 121	isfsuppd	$⊢ φ \to {finSupp}_{0_{U}} ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})))$
123	16 106 107 15 51	mplelbas	$⊢ (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)} \leftrightarrow ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPwSer U)} \land {finSupp}_{0_{U}} ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))))$
124	109 122 123	sylanbrc	$⊢ φ \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)}$
125	124	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)}$
126		eqid	$⊢ {Base}_{Scalar (I mPoly U)} = {Base}_{Scalar (I mPoly U)}$
127		eqid	$⊢ \cdot_{(I mPoly U)} = \cdot_{(I mPoly U)}$
128		eqid	$⊢ \cdot_{(I mPoly U)} = \cdot_{(I mPoly U)}$
129	26 27 126 51 127 128	asclmul1	$⊢ (I mPoly U \in AssAlg \land b \in {Base}_{Scalar (I mPoly U)} \land (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)}) \to algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = b \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
130	90 94 125 129	syl3anc	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = b \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
131		simprr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to b \in {Base}_{U}$
132	16 128 14 51 47 18 131 125	mplvsca	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to b \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) {\cdot_{U}}_{f} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
133	130 132	eqtrd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) {\cdot_{U}}_{f} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
134		vex	$⊢ b \in V$
135		fnconstg	$⊢ b \in V \to (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) Fn \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
136	134 135	mp1i	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) Fn \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
137		fvex	$⊢ 1_{U} \in V$
138		fvex	$⊢ 0_{U} \in V$
139	137 138	ifex	$⊢ if (w = a, 1_{U}, 0_{U}) \in V$
140		eqid	$⊢ (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))$
141	139 140	fnmpti	$⊢ (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) Fn \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
142	141	a1i	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) Fn \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
143	97	a1i	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \in V$
144		inidm	$⊢ \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \cap \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
145	134	fvconst2	$⊢ s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \to (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) (s) = b$
146	145	adantl	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) (s) = b$
147		equequ1	$⊢ w = s \to (w = a \leftrightarrow s = a)$
148	147	ifbid	$⊢ w = s \to if (w = a, 1_{U}, 0_{U}) = if (s = a, 1_{U}, 0_{U})$
149	137 138	ifex	$⊢ if (s = a, 1_{U}, 0_{U}) \in V$
150	148 140 149	fvmpt	$⊢ s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) (s) = if (s = a, 1_{U}, 0_{U})$
151	150	adantl	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) (s) = if (s = a, 1_{U}, 0_{U})$
152	136 142 143 143 144 146 151	offval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (\{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \times \{b\}) {\cdot_{U}}_{f} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = (s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ b \cdot_{U} if (s = a, 1_{U}, 0_{U}))$
153		ovif2	$⊢ b \cdot_{U} if (s = a, 1_{U}, 0_{U}) = if (s = a, b \cdot_{U} 1_{U}, b \cdot_{U} 0_{U})$
154	21	ad2antrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to U \in Ring$
155		simplrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to b \in {Base}_{U}$
156	14 47 99	ringridm	$⊢ (U \in Ring \land b \in {Base}_{U}) \to b \cdot_{U} 1_{U} = b$
157	154 155 156	syl2anc	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to b \cdot_{U} 1_{U} = b$
158	14 47 15	ringrz	$⊢ (U \in Ring \land b \in {Base}_{U}) \to b \cdot_{U} 0_{U} = 0_{U}$
159	154 155 158	syl2anc	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to b \cdot_{U} 0_{U} = 0_{U}$
160	157 159	ifeq12d	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to if (s = a, b \cdot_{U} 1_{U}, b \cdot_{U} 0_{U}) = if (s = a, b, 0_{U})$
161	153 160	syl5eq	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to b \cdot_{U} if (s = a, 1_{U}, 0_{U}) = if (s = a, b, 0_{U})$
162	161	mpteq2dva	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ b \cdot_{U} if (s = a, 1_{U}, 0_{U})) = (s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (s = a, b, 0_{U}))$
163	133 152 162	3eqtrd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) = (s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (s = a, b, 0_{U}))$
164	7	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to I \in V$
165	8	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to S \in CRing$
166	9	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to R \in SubRing (S)$
167	73	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (I \times \{L\}) {\underset{˙}{\cdot}}_{f} A \in (K^{I})$
168	21	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to U \in Ring$
169	16 51 14 26 164 168	mplasclf	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to algSc (I mPoly U) : {Base}_{U} ⟶ {Base}_{(I mPoly U)}$
170	169 131	ffvelrnd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to algSc (I mPoly U) (b) \in {Base}_{(I mPoly U)}$
171		eqidd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
172	170 171	jca	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (algSc (I mPoly U) (b) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A))$
173		elrabi	$⊢ a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \to a \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
174	173	ad2antrl	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to a \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
175	1 16 3 51 4 39 6 15 99 18 140 164 165 166 167 174	evlsbagval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)} \land Q ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v)))$
176	1 16 3 4 51 164 165 166 167 172 175 127 5	evlsmulval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v))))$
177	176	simprd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v)))$
178	39	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
179	60 178	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
180	39 4	mgpbas	$⊢ K = {Base}_{{mulGrp}_{S}}$
181	180 6	mulgnn0cl	$⊢ ({mulGrp}_{S} \in Mnd \land N \in ℕ_{0} \land L \in K) \to N \underset{˙}{\times} L \in K$
182	179 11 66 181	syl3anc	$⊢ φ \to N \underset{˙}{\times} L \in K$
183	182	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to N \underset{˙}{\times} L \in K$
184	45 65	eqsstrrd	$⊢ φ \to {Base}_{U} \subseteq K$
185	184	sselda	$⊢ (φ \land b \in {Base}_{U}) \to b \in K$
186	185	adantrl	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to b \in K$
187	4 5	crngcom	$⊢ (S \in CRing \land N \underset{˙}{\times} L \in K \land b \in K) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} b = b \underset{˙}{\cdot} (N \underset{˙}{\times} L)$
188	165 183 186 187	syl3anc	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} b = b \underset{˙}{\cdot} (N \underset{˙}{\times} L)$
189	188	oveq1d	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to ((N \underset{˙}{\times} L) \underset{˙}{\cdot} b) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))) = (b \underset{˙}{\cdot} (N \underset{˙}{\times} L)) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
190	165	crngringd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to S \in Ring$
191		eqid	$⊢ 1_{S} = 1_{S}$
192	39 191	ringidval	$⊢ 1_{S} = 0_{{mulGrp}_{S}}$
193	39	crngmgp	$⊢ S \in CRing \to {mulGrp}_{S} \in CMnd$
194	8 193	syl	$⊢ φ \to {mulGrp}_{S} \in CMnd$
195	194	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to {mulGrp}_{S} \in CMnd$
196	179	ad2antrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to {mulGrp}_{S} \in Mnd$
197		elrabi	$⊢ a \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \to a \in ({ℕ_{0}}^{I})$
198		elmapi	$⊢ a \in ({ℕ_{0}}^{I}) \to a : I ⟶ ℕ_{0}$
199	173 197 198	3syl	$⊢ a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \to a : I ⟶ ℕ_{0}$
200	199	adantl	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to a : I ⟶ ℕ_{0}$
201	200	adantrr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to a : I ⟶ ℕ_{0}$
202	201	ffvelrnda	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to a (v) \in ℕ_{0}$
203	70	ad2antrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to A : I ⟶ K$
204		simpr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to v \in I$
205	203 204	ffvelrnd	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to A (v) \in K$
206	180 6	mulgnn0cl	$⊢ ({mulGrp}_{S} \in Mnd \land a (v) \in ℕ_{0} \land A (v) \in K) \to a (v) \underset{˙}{\times} A (v) \in K$
207	196 202 205 206	syl3anc	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to a (v) \underset{˙}{\times} A (v) \in K$
208	207	fmpttd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) : I ⟶ K$
209	18	psrbagfsupp	$⊢ a \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \to {finSupp}_{0} (a)$
210	209	adantl	$⊢ (φ \land a \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to {finSupp}_{0} (a)$
211	210	fsuppimpd	$⊢ (φ \land a \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}) \to a supp 0 \in Fin$
212	173 211	sylan2	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to a supp 0 \in Fin$
213	212	adantrr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to a supp 0 \in Fin$
214	201	feqmptd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to a = (v \in I ⟼ a (v))$
215	214	oveq1d	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to a supp 0 = (v \in I ⟼ a (v)) supp 0$
216		ssidd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to a supp 0 \subseteq a supp 0$
217	215 216	eqsstrrd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (v \in I ⟼ a (v)) supp 0 \subseteq a supp 0$
218	180 192 6	mulg0	$⊢ k \in K \to 0 \underset{˙}{\times} k = 1_{S}$
219	218	adantl	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land k \in K) \to 0 \underset{˙}{\times} k = 1_{S}$
220		c0ex	$⊢ 0 \in V$
221	220	a1i	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to 0 \in V$
222	217 219 202 205 221	suppssov1	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) supp 1_{S} \subseteq a supp 0$
223	213 222	ssfid	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) supp 1_{S} \in Fin$
224	180 192 195 164 208 223	gsumcl2	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} A (v)) \in K$
225	4 5	ringass	$⊢ (S \in Ring \land (N \underset{˙}{\times} L \in K \land b \in K \land \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} A (v)) \in K)) \to ((N \underset{˙}{\times} L) \underset{˙}{\cdot} b) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (b \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
226	190 183 186 224 225	syl13anc	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to ((N \underset{˙}{\times} L) \underset{˙}{\cdot} b) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (b \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
227	4 5	ringass	$⊢ (S \in Ring \land (b \in K \land N \underset{˙}{\times} L \in K \land \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} A (v)) \in K)) \to (b \underset{˙}{\cdot} (N \underset{˙}{\times} L)) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))) = b \underset{˙}{\cdot} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
228	190 186 183 224 227	syl13anc	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (b \underset{˙}{\cdot} (N \underset{˙}{\times} L)) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))) = b \underset{˙}{\cdot} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
229	189 226 228	3eqtr3d	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} (b \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))) = b \underset{˙}{\cdot} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
230	13	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to A \in (K^{I})$
231	45	eleq2d	$⊢ φ \to (b \in R \leftrightarrow b \in {Base}_{U})$
232	231	biimpar	$⊢ (φ \land b \in {Base}_{U}) \to b \in R$
233	232	adantrl	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to b \in R$
234	1 16 3 4 51 26 164 165 166 233 230	evlsscaval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (algSc (I mPoly U) (b) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (b)) (A) = b)$
235	1 16 3 51 4 39 6 15 99 18 140 164 165 166 230 174	evlsbagval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)} \land Q ((w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A) = \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} A (v)))$
236	1 16 3 4 51 164 165 166 230 234 235 127 5	evlsmulval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A) = b \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
237	236	simprd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A) = b \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
238	237	oveq2d	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (b \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
239	1 16 3 4 51 26 164 165 166 233 167	evlsscaval	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (algSc (I mPoly U) (b) \in {Base}_{(I mPoly U)} \land Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = b)$
240	239	simprd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = b$
241		fconst6g	$⊢ L \in R \to (I \times \{L\}) : I ⟶ R$
242	10 241	syl	$⊢ φ \to (I \times \{L\}) : I ⟶ R$
243	242	ffnd	$⊢ φ \to (I \times \{L\}) Fn I$
244	243	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (I \times \{L\}) Fn I$
245	70	ffnd	$⊢ φ \to A Fn I$
246	245	adantr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to A Fn I$
247	10	ad2antrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to L \in R$
248		fvconst2g	$⊢ (L \in R \land v \in I) \to (I \times \{L\}) (v) = L$
249	247 204 248	syl2anc	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to (I \times \{L\}) (v) = L$
250		eqidd	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to A (v) = A (v)$
251	244 246 164 164 71 249 250	ofval	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v) = L \underset{˙}{\cdot} A (v)$
252	251	oveq2d	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v) = a (v) \underset{˙}{\times} (L \underset{˙}{\cdot} A (v))$
253	194	ad2antrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to {mulGrp}_{S} \in CMnd$
254	66	ad2antrr	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to L \in K$
255	39 5	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{S}}$
256	180 6 255	mulgnn0di	$⊢ ({mulGrp}_{S} \in CMnd \land (a (v) \in ℕ_{0} \land L \in K \land A (v) \in K)) \to a (v) \underset{˙}{\times} (L \underset{˙}{\cdot} A (v)) = (a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v))$
257	253 202 254 205 256	syl13anc	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to a (v) \underset{˙}{\times} (L \underset{˙}{\cdot} A (v)) = (a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v))$
258	252 257	eqtrd	$⊢ ((φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \land v \in I) \to a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v) = (a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v))$
259	258	mpteq2dva	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (v \in I ⟼ a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v)) = (v \in I ⟼ (a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v)))$
260	259	oveq2d	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v)) = \underset{v \in I}{\sum_{{mulGrp}_{S}}} ((a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v)))$
261	194	adantr	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to {mulGrp}_{S} \in CMnd$
262	7	adantr	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to I \in V$
263	179	ad2antrr	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land v \in I) \to {mulGrp}_{S} \in Mnd$
264	200	ffvelrnda	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land v \in I) \to a (v) \in ℕ_{0}$
265	66	ad2antrr	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land v \in I) \to L \in K$
266	180 6	mulgnn0cl	$⊢ ({mulGrp}_{S} \in Mnd \land a (v) \in ℕ_{0} \land L \in K) \to a (v) \underset{˙}{\times} L \in K$
267	263 264 265 266	syl3anc	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land v \in I) \to a (v) \underset{˙}{\times} L \in K$
268	70	ffvelrnda	$⊢ (φ \land v \in I) \to A (v) \in K$
269	268	adantlr	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land v \in I) \to A (v) \in K$
270	263 264 269 206	syl3anc	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land v \in I) \to a (v) \underset{˙}{\times} A (v) \in K$
271		eqidd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} L) = (v \in I ⟼ a (v) \underset{˙}{\times} L)$
272		eqidd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) = (v \in I ⟼ a (v) \underset{˙}{\times} A (v))$
273	262	mptexd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} L) \in V$
274		fvexd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to 1_{S} \in V$
275		funmpt	$⊢ Fun (v \in I ⟼ a (v) \underset{˙}{\times} L)$
276	275	a1i	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to Fun (v \in I ⟼ a (v) \underset{˙}{\times} L)$
277	200	feqmptd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to a = (v \in I ⟼ a (v))$
278	277	oveq1d	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to a supp 0 = (v \in I ⟼ a (v)) supp 0$
279		ssidd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to a supp 0 \subseteq a supp 0$
280	278 279	eqsstrrd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v)) supp 0 \subseteq a supp 0$
281	218	adantl	$⊢ ((φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \land k \in K) \to 0 \underset{˙}{\times} k = 1_{S}$
282	220	a1i	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to 0 \in V$
283	280 281 264 265 282	suppssov1	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} L) supp 1_{S} \subseteq a supp 0$
284	212 283	ssfid	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} L) supp 1_{S} \in Fin$
285	273 274 276 284	isfsuppd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to {finSupp}_{1_{S}} ((v \in I ⟼ a (v) \underset{˙}{\times} L))$
286	262	mptexd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) \in V$
287		funmpt	$⊢ Fun (v \in I ⟼ a (v) \underset{˙}{\times} A (v))$
288	287	a1i	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to Fun (v \in I ⟼ a (v) \underset{˙}{\times} A (v))$
289	280 281 264 269 282	suppssov1	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) supp 1_{S} \subseteq a supp 0$
290	212 289	ssfid	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (v \in I ⟼ a (v) \underset{˙}{\times} A (v)) supp 1_{S} \in Fin$
291	286 274 288 290	isfsuppd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to {finSupp}_{1_{S}} ((v \in I ⟼ a (v) \underset{˙}{\times} A (v)))$
292	180 192 255 261 262 267 270 271 272 285 291	gsummptfsadd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} ((a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v))) = (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} L)) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
293	18 19 180 6 7 179 66 11	mhphflem	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} L) = N \underset{˙}{\times} L$
294	293	oveq1d	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} L)) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
295	292 294	eqtrd	$⊢ (φ \land a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} ((a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v))) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
296	295	adantrr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} ((a (v) \underset{˙}{\times} L) \underset{˙}{\cdot} (a (v) \underset{˙}{\times} A (v))) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
297	260 296	eqtrd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to \underset{v \in I}{\sum_{{mulGrp}_{S}}} (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v)) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v)))$
298	240 297	oveq12d	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v))) = b \underset{˙}{\cdot} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} A (v))))$
299	229 238 298	3eqtr4rd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b)) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) \underset{˙}{\cdot} (\underset{v \in I}{\sum_{{mulGrp}_{S}}}, (a (v) \underset{˙}{\times} ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) (v))) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A)$
300	177 299	eqtrd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A)$
301		ovex	$⊢ algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in V$
302		fveq2	$⊢ f = algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \to Q (f) = Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})))$
303	302	fveq1d	$⊢ f = algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \to Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
304	302	fveq1d	$⊢ f = algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \to Q (f) (A) = Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A)$
305	304	oveq2d	$⊢ f = algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A)$
306	303 305	eqeq12d	$⊢ f = algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \to (Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) \leftrightarrow Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A))$
307	301 306	elab	$⊢ algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U}))) (A)$
308	300 307	sylibr	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to algSc (I mPoly U) (b) \cdot_{(I mPoly U)} (w \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (w = a, 1_{U}, 0_{U})) \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
309	163 308	eqeltrrd	$⊢ (φ \land (a \in \{g \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in {Base}_{U})) \to (s \in \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (s = a, b, 0_{U})) \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
310		elin	$⊢ x \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \leftrightarrow (x \in H (N) \land x \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\})$
311		vex	$⊢ x \in V$
312		fveq2	$⊢ f = x \to Q (f) = Q (x)$
313	312	fveq1d	$⊢ f = x \to Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
314	312	fveq1d	$⊢ f = x \to Q (f) (A) = Q (x) (A)$
315	314	oveq2d	$⊢ f = x \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)$
316	313 315	eqeq12d	$⊢ f = x \to (Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) \leftrightarrow Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))$
317	311 316	elab	$⊢ x \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)$
318	317	anbi2i	$⊢ (x \in H (N) \land x \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \leftrightarrow (x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))$
319	310 318	bitri	$⊢ x \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \leftrightarrow (x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))$
320		elin	$⊢ y \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \leftrightarrow (y \in H (N) \land y \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\})$
321		vex	$⊢ y \in V$
322		fveq2	$⊢ f = y \to Q (f) = Q (y)$
323	322	fveq1d	$⊢ f = y \to Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
324	322	fveq1d	$⊢ f = y \to Q (f) (A) = Q (y) (A)$
325	324	oveq2d	$⊢ f = y \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)$
326	323 325	eqeq12d	$⊢ f = y \to (Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) \leftrightarrow Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
327	321 326	elab	$⊢ y \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)$
328	327	anbi2i	$⊢ (y \in H (N) \land y \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \leftrightarrow (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
329	320 328	bitri	$⊢ y \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \leftrightarrow (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
330	319 329	anbi12i	$⊢ (x \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \land y \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\})) \leftrightarrow ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))$
331	60	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to S \in Ring$
332	182	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to N \underset{˙}{\times} L \in K$
333		eqid	$⊢ S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)} = S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)}$
334		eqid	$⊢ {Base}_{(S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)})} = {Base}_{(S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)})}$
335	8	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to S \in CRing$
336		fvexd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to {Base}_{(S ↑_{𝑠} I)} \in V$
337		eqid	$⊢ S ↑_{𝑠} (K^{I}) = S ↑_{𝑠} (K^{I})$
338	1 16 3 337 4	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in ((I mPoly U) RingHom (S ↑_{𝑠} (K^{I})))$
339	7 8 9 338	syl3anc	$⊢ φ \to Q \in ((I mPoly U) RingHom (S ↑_{𝑠} (K^{I})))$
340		eqid	$⊢ {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} (K^{I}))}$
341	51 340	rhmf	$⊢ Q \in ((I mPoly U) RingHom (S ↑_{𝑠} (K^{I}))) \to Q : {Base}_{(I mPoly U)} ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
342	339 341	syl	$⊢ φ \to Q : {Base}_{(I mPoly U)} ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
343	342	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q : {Base}_{(I mPoly U)} ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
344	7	adantr	$⊢ (φ \land x \in H (N)) \to I \in V$
345	21	adantr	$⊢ (φ \land x \in H (N)) \to U \in Ring$
346	11	adantr	$⊢ (φ \land x \in H (N)) \to N \in ℕ_{0}$
347		simpr	$⊢ (φ \land x \in H (N)) \to x \in H (N)$
348	2 16 51 344 345 346 347	mhpmpl	$⊢ (φ \land x \in H (N)) \to x \in {Base}_{(I mPoly U)}$
349	348	adantrr	$⊢ (φ \land (x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))) \to x \in {Base}_{(I mPoly U)}$
350	349	adantrr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to x \in {Base}_{(I mPoly U)}$
351	343 350	ffvelrnd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
352		eqid	$⊢ S ↑_{𝑠} I = S ↑_{𝑠} I$
353	352 4	pwsbas	$⊢ (S \in CRing \land I \in V) \to K^{I} = {Base}_{(S ↑_{𝑠} I)}$
354	8 7 353	syl2anc	$⊢ φ \to K^{I} = {Base}_{(S ↑_{𝑠} I)}$
355	354	oveq2d	$⊢ φ \to S ↑_{𝑠} (K^{I}) = S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)}$
356	355	fveq2d	$⊢ φ \to {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)})}$
357	356	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)})}$
358	351 357	eleqtrd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x) \in {Base}_{(S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)})}$
359	333 4 334 335 336 358	pwselbas	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x) : {Base}_{(S ↑_{𝑠} I)} ⟶ K$
360	13 354	eleqtrd	$⊢ φ \to A \in {Base}_{(S ↑_{𝑠} I)}$
361	360	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to A \in {Base}_{(S ↑_{𝑠} I)}$
362	359 361	ffvelrnd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x) (A) \in K$
363	7	adantr	$⊢ (φ \land y \in H (N)) \to I \in V$
364	21	adantr	$⊢ (φ \land y \in H (N)) \to U \in Ring$
365	11	adantr	$⊢ (φ \land y \in H (N)) \to N \in ℕ_{0}$
366		simpr	$⊢ (φ \land y \in H (N)) \to y \in H (N)$
367	2 16 51 363 364 365 366	mhpmpl	$⊢ (φ \land y \in H (N)) \to y \in {Base}_{(I mPoly U)}$
368	367	adantrr	$⊢ (φ \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))) \to y \in {Base}_{(I mPoly U)}$
369	368	adantrl	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to y \in {Base}_{(I mPoly U)}$
370	343 369	ffvelrnd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (y) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
371	370 357	eleqtrd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (y) \in {Base}_{(S ↑_{𝑠} {Base}_{(S ↑_{𝑠} I)})}$
372	333 4 334 335 336 371	pwselbas	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (y) : {Base}_{(S ↑_{𝑠} I)} ⟶ K$
373	372 361	ffvelrnd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (y) (A) \in K$
374		eqid	$⊢ +_{S} = +_{S}$
375	4 374 5	ringdi	$⊢ (S \in Ring \land (N \underset{˙}{\times} L \in K \land Q (x) (A) \in K \land Q (y) (A) \in K)) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} (Q (x) (A) +_{S} Q (y) (A)) = ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) +_{S} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
376	331 332 362 373 375	syl13anc	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} (Q (x) (A) +_{S} Q (y) (A)) = ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) +_{S} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
377	7	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to I \in V$
378	9	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to R \in SubRing (S)$
379	13	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to A \in (K^{I})$
380		eqidd	$⊢ (φ \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \to Q (x) (A) = Q (x) (A)$
381	348 380	anim12dan	$⊢ (φ \land (x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))) \to (x \in {Base}_{(I mPoly U)} \land Q (x) (A) = Q (x) (A))$
382	381	adantrr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (x \in {Base}_{(I mPoly U)} \land Q (x) (A) = Q (x) (A))$
383		eqidd	$⊢ (φ \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)) \to Q (y) (A) = Q (y) (A)$
384	367 383	anim12dan	$⊢ (φ \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))) \to (y \in {Base}_{(I mPoly U)} \land Q (y) (A) = Q (y) (A))$
385	384	adantrl	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (y \in {Base}_{(I mPoly U)} \land Q (y) (A) = Q (y) (A))$
386	1 16 3 4 51 377 335 378 379 382 385 17 374	evlsaddval	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (x +_{(I mPoly U)} y \in {Base}_{(I mPoly U)} \land Q (x +_{(I mPoly U)} y) (A) = Q (x) (A) +_{S} Q (y) (A))$
387	386	simprd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x +_{(I mPoly U)} y) (A) = Q (x) (A) +_{S} Q (y) (A)$
388	387	oveq2d	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x +_{(I mPoly U)} y) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} (Q (x) (A) +_{S} Q (y) (A))$
389	58	a1i	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to K \in V$
390	63	adantlr	$⊢ ((φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \land (j \in K \land k \in K)) \to j \underset{˙}{\cdot} k \in K$
391	68	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (I \times \{L\}) : I ⟶ K$
392	70	adantr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to A : I ⟶ K$
393	390 391 392 377 377 71	off	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) : I ⟶ K$
394	389 377 393	elmapdd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (I \times \{L\}) {\underset{˙}{\cdot}}_{f} A \in (K^{I})$
395		simpr	$⊢ (φ \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \to Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)$
396	348 395	anim12dan	$⊢ (φ \land (x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))) \to (x \in {Base}_{(I mPoly U)} \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))$
397	396	adantrr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (x \in {Base}_{(I mPoly U)} \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A))$
398		simpr	$⊢ (φ \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)) \to Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)$
399	367 398	anim12dan	$⊢ (φ \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))) \to (y \in {Base}_{(I mPoly U)} \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
400	399	adantrl	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (y \in {Base}_{(I mPoly U)} \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
401	1 16 3 4 51 377 335 378 394 397 400 17 374	evlsaddval	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to (x +_{(I mPoly U)} y \in {Base}_{(I mPoly U)} \land Q (x +_{(I mPoly U)} y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) +_{S} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))$
402	401	simprd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x +_{(I mPoly U)} y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) +_{S} ((N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A))$
403	376 388 402	3eqtr4rd	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to Q (x +_{(I mPoly U)} y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x +_{(I mPoly U)} y) (A)$
404		ovex	$⊢ x +_{(I mPoly U)} y \in V$
405		fveq2	$⊢ f = x +_{(I mPoly U)} y \to Q (f) = Q (x +_{(I mPoly U)} y)$
406	405	fveq1d	$⊢ f = x +_{(I mPoly U)} y \to Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (x +_{(I mPoly U)} y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
407	405	fveq1d	$⊢ f = x +_{(I mPoly U)} y \to Q (f) (A) = Q (x +_{(I mPoly U)} y) (A)$
408	407	oveq2d	$⊢ f = x +_{(I mPoly U)} y \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x +_{(I mPoly U)} y) (A)$
409	406 408	eqeq12d	$⊢ f = x +_{(I mPoly U)} y \to (Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) \leftrightarrow Q (x +_{(I mPoly U)} y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x +_{(I mPoly U)} y) (A))$
410	404 409	elab	$⊢ x +_{(I mPoly U)} y \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (x +_{(I mPoly U)} y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x +_{(I mPoly U)} y) (A)$
411	403 410	sylibr	$⊢ (φ \land ((x \in H (N) \land Q (x) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (x) (A)) \land (y \in H (N) \land Q (y) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (y) (A)))) \to x +_{(I mPoly U)} y \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
412	330 411	sylan2b	$⊢ (φ \land (x \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}) \land y \in (H (N) \cap \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}))) \to x +_{(I mPoly U)} y \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
413	2 14 15 16 17 18 19 7 22 11 12 85 309 412	mhpind	$⊢ φ \to X \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\}$
414		fveq2	$⊢ f = X \to Q (f) = Q (X)$
415	414	fveq1d	$⊢ f = X \to Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = Q (X) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A)$
416	414	fveq1d	$⊢ f = X \to Q (f) (A) = Q (X) (A)$
417	416	oveq2d	$⊢ f = X \to (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A)$
418	415 417	eqeq12d	$⊢ f = X \to (Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A) \leftrightarrow Q (X) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A))$
419	418	elabg	$⊢ X \in H (N) \to (X \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (X) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A))$
420	12 419	syl	$⊢ φ \to (X \in \{f \| Q (f) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (f) (A)\} \leftrightarrow Q (X) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A))$
421	413 420	mpbid	$⊢ φ \to Q (X) ((I \times \{L\}) {\underset{˙}{\cdot}}_{f} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A)$

Metamath Proof Explorer

Theorem mhphf

Proof