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