extvfvcl

Description: Closure for the "variable extension" function evaluated for converting a given polynomial F by adding a variable with index A . (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	extvfvvcl.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	extvfvvcl.3	$⊢ \underset{˙}{0} = 0_{R}$
	extvfvvcl.i	$⊢ φ \to I \in V$
	extvfvvcl.r	$⊢ φ \to R \in Ring$
	extvfvvcl.b	$⊢ B = {Base}_{R}$
	extvfvvcl.j	$⊢ J = I ∖ \{A\}$
	extvfvvcl.m	$⊢ M = {Base}_{(J mPoly R)}$
	extvfvvcl.1	$⊢ φ \to A \in I$
	extvfvvcl.f	$⊢ φ \to F \in M$
	extvfvcl.n	$⊢ N = {Base}_{(I mPoly R)}$
Assertion	extvfvcl	Could not format assertion : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		extvfvvcl.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
2		extvfvvcl.3	$⊢ \underset{˙}{0} = 0_{R}$
3		extvfvvcl.i	$⊢ φ \to I \in V$
4		extvfvvcl.r	$⊢ φ \to R \in Ring$
5		extvfvvcl.b	$⊢ B = {Base}_{R}$
6		extvfvvcl.j	$⊢ J = I ∖ \{A\}$
7		extvfvvcl.m	$⊢ M = {Base}_{(J mPoly R)}$
8		extvfvvcl.1	$⊢ φ \to A \in I$
9		extvfvvcl.f	$⊢ φ \to F \in M$
10		extvfvcl.n	$⊢ N = {Base}_{(I mPoly R)}$
11	5	fvexi	$⊢ B \in V$
12	11	a1i	$⊢ φ \to B \in V$
13		ovex	$⊢ {ℕ_{0}}^{I} \in V$
14	1 13	rabex2	$⊢ D \in V$
15	14	a1i	$⊢ φ \to D \in V$
16		fvexd	$⊢ (φ \land x \in D) \to F ({x ↾}_{J}) \in V$
17	2	fvexi	$⊢ \underset{˙}{0} \in V$
18	17	a1i	$⊢ (φ \land x \in D) \to \underset{˙}{0} \in V$
19	16 18	ifcld	$⊢ (φ \land x \in D) \to if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0}) \in V$
20	1 2 3 4 8 6 7 9	extvfv	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D \|-> if ( ( x ` A ) = 0 , ( F ` ( x \|` J ) ) , .0. ) ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D \|-> if ( ( x ` A ) = 0 , ( F ` ( x \|` J ) ) , .0. ) ) ) with typecode \|-
21	3	adantr	$⊢ (φ \land x \in D) \to I \in V$
22	4	adantr	$⊢ (φ \land x \in D) \to R \in Ring$
23	8	adantr	$⊢ (φ \land x \in D) \to A \in I$
24	9	adantr	$⊢ (φ \land x \in D) \to F \in M$
25		simpr	$⊢ (φ \land x \in D) \to x \in D$
26	1 2 21 22 5 6 7 23 24 25	extvfvvcl	Could not format ( ( ph /\ x e. D ) -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` x ) e. B ) : No typesetting found for \|- ( ( ph /\ x e. D ) -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` x ) e. B ) with typecode \|-
27	19 20 26	fmpt2d	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) : D --> B ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) : D --> B ) with typecode \|-
28	12 15 27	elmapdd	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( B ^m D ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( B ^m D ) ) with typecode \|-
29		eqid	$⊢ I mPwSer R = I mPwSer R$
30	1	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
31		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
32	29 5 30 31 3	psrbas	$⊢ φ \to {Base}_{(I mPwSer R)} = B^{D}$
33	28 32	eleqtrrd	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) ) with typecode \|-
34	15	mptexd	$⊢ φ \to (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})) \in V$
35	17	a1i	$⊢ φ \to \underset{˙}{0} \in V$
36	19	fmpttd	$⊢ φ \to (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})) : D ⟶ V$
37	36	ffund	$⊢ φ \to Fun (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0}))$
38		fveq1	$⊢ y = x \to y (A) = x (A)$
39	38	eqeq1d	$⊢ y = x \to (y (A) = 0 \leftrightarrow x (A) = 0)$
40	39	cbvrabv	$⊢ \{y \in D \| y (A) = 0\} = \{x \in D \| x (A) = 0\}$
41	40	partfun2	$⊢ (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})) = (x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J})) \cup (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0})$
42	41	oveq1i	$⊢ (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})) supp \underset{˙}{0} = ((x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J})) \cup (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0})) supp \underset{˙}{0}$
43	40 15	rabexd	$⊢ φ \to \{y \in D \| y (A) = 0\} \in V$
44	43	mptexd	$⊢ φ \to (x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J})) \in V$
45	15	difexd	$⊢ φ \to D ∖ \{y \in D \| y (A) = 0\} \in V$
46	45	mptexd	$⊢ φ \to (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}) \in V$
47	44 46 35	suppun2	$⊢ φ \to ((x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J})) \cup (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0})) supp \underset{˙}{0} = {supp}_{\underset{˙}{0}} ((x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J}))) \cup {supp}_{\underset{˙}{0}} ((x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}))$
48	42 47	eqtrid	$⊢ φ \to (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})) supp \underset{˙}{0} = {supp}_{\underset{˙}{0}} ((x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J}))) \cup {supp}_{\underset{˙}{0}} ((x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}))$
49		eqid	$⊢ J mPoly R = J mPoly R$
50		eqid	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
51	50	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{J}) \| h^{-1} [ℕ] \in Fin\}$
52	49 5 7 51 9	mplelf	$⊢ φ \to F : \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟶ B$
53		breq1	$⊢ h = {x ↾}_{J} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (({x ↾}_{J})))$
54		nn0ex	$⊢ ℕ_{0} \in V$
55	54	a1i	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to ℕ_{0} \in V$
56	3	difexd	$⊢ φ \to I ∖ \{A\} \in V$
57	6 56	eqeltrid	$⊢ φ \to J \in V$
58	57	adantr	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to J \in V$
59	3	adantr	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to I \in V$
60		ssrab2	$⊢ \{y \in D \| y (A) = 0\} \subseteq D$
61		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
62	61	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
63	1 62	eqsstrid	$⊢ φ \to D \subseteq {ℕ_{0}}^{I}$
64	60 63	sstrid	$⊢ φ \to \{y \in D \| y (A) = 0\} \subseteq {ℕ_{0}}^{I}$
65	64	sselda	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to x \in ({ℕ_{0}}^{I})$
66	59 55 65	elmaprd	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to x : I ⟶ ℕ_{0}$
67		difssd	$⊢ φ \to I ∖ \{A\} \subseteq I$
68	6 67	eqsstrid	$⊢ φ \to J \subseteq I$
69	68	adantr	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to J \subseteq I$
70	66 69	fssresd	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to ({x ↾}_{J}) : J ⟶ ℕ_{0}$
71	55 58 70	elmapdd	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to {x ↾}_{J} \in ({ℕ_{0}}^{J})$
72	60	a1i	$⊢ φ \to \{y \in D \| y (A) = 0\} \subseteq D$
73	72	sselda	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to x \in D$
74	30	psrbagfsupp	$⊢ x \in D \to {finSupp}_{0} (x)$
75	73 74	syl	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to {finSupp}_{0} (x)$
76		c0ex	$⊢ 0 \in V$
77	76	a1i	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to 0 \in V$
78	75 77	fsuppres	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to {finSupp}_{0} (({x ↾}_{J}))$
79	53 71 78	elrabd	$⊢ (φ \land x \in \{y \in D \| y (A) = 0\}) \to {x ↾}_{J} \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
80	52 79	cofmpt	$⊢ φ \to F \circ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) = (x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J}))$
81	80	oveq1d	$⊢ φ \to (F \circ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})) supp \underset{˙}{0} = (x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J})) supp \underset{˙}{0}$
82	43	mptexd	$⊢ φ \to (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) \in V$
83		suppco	$⊢ (F \in M \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) \in V) \to (F \circ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})) supp \underset{˙}{0} = {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1} [F supp \underset{˙}{0}]$
84	9 82 83	syl2anc	$⊢ φ \to (F \circ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})) supp \underset{˙}{0} = {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1} [F supp \underset{˙}{0}]$
85	71	fmpttd	$⊢ φ \to (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} ⟶ {ℕ_{0}}^{J}$
86		simpr	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)$
87		eqid	$⊢ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})$
88		reseq1	$⊢ x = u \to {x ↾}_{J} = {u ↾}_{J}$
89		simpllr	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u \in \{y \in D \| y (A) = 0\}$
90	89	resexd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to {u ↾}_{J} \in V$
91	87 88 89 90	fvmptd3	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = {u ↾}_{J}$
92		reseq1	$⊢ x = v \to {x ↾}_{J} = {v ↾}_{J}$
93		simplr	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v \in \{y \in D \| y (A) = 0\}$
94	93	resexd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to {v ↾}_{J} \in V$
95	87 92 93 94	fvmptd3	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v) = {v ↾}_{J}$
96	86 91 95	3eqtr3d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to {u ↾}_{J} = {v ↾}_{J}$
97	6	a1i	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to J = I ∖ \{A\}$
98	97	reseq2d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to {u ↾}_{J} = {u ↾}_{(I ∖ \{A\})}$
99	97	reseq2d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to {v ↾}_{J} = {v ↾}_{(I ∖ \{A\})}$
100	96 98 99	3eqtr3d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to {u ↾}_{(I ∖ \{A\})} = {v ↾}_{(I ∖ \{A\})}$
101		fveq1	$⊢ y = u \to y (A) = u (A)$
102	101	eqeq1d	$⊢ y = u \to (y (A) = 0 \leftrightarrow u (A) = 0)$
103	102 89	elrabrd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u (A) = 0$
104		fveq1	$⊢ y = v \to y (A) = v (A)$
105	104	eqeq1d	$⊢ y = v \to (y (A) = 0 \leftrightarrow v (A) = 0)$
106	105 93	elrabrd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v (A) = 0$
107	103 106	eqtr4d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u (A) = v (A)$
108	107	opeq2d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to ⟨A, u (A)⟩ = ⟨A, v (A)⟩$
109	108	sneqd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to \{⟨A, u (A)⟩\} = \{⟨A, v (A)⟩\}$
110	100 109	uneq12d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to ({u ↾}_{(I ∖ \{A\})}) \cup \{⟨A, u (A)⟩\} = ({v ↾}_{(I ∖ \{A\})}) \cup \{⟨A, v (A)⟩\}$
111	3	ad3antrrr	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to I \in V$
112	54	a1i	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to ℕ_{0} \in V$
113	63	ad3antrrr	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to D \subseteq {ℕ_{0}}^{I}$
114	60 89	sselid	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u \in D$
115	113 114	sseldd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u \in ({ℕ_{0}}^{I})$
116	111 112 115	elmaprd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u : I ⟶ ℕ_{0}$
117	116	ffnd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u Fn I$
118	8	ad3antrrr	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to A \in I$
119		fnsnsplit	$⊢ (u Fn I \land A \in I) \to u = ({u ↾}_{(I ∖ \{A\})}) \cup \{⟨A, u (A)⟩\}$
120	117 118 119	syl2anc	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u = ({u ↾}_{(I ∖ \{A\})}) \cup \{⟨A, u (A)⟩\}$
121	60 93	sselid	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v \in D$
122	113 121	sseldd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v \in ({ℕ_{0}}^{I})$
123	111 112 122	elmaprd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v : I ⟶ ℕ_{0}$
124	123	ffnd	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v Fn I$
125		fnsnsplit	$⊢ (v Fn I \land A \in I) \to v = ({v ↾}_{(I ∖ \{A\})}) \cup \{⟨A, v (A)⟩\}$
126	124 118 125	syl2anc	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to v = ({v ↾}_{(I ∖ \{A\})}) \cup \{⟨A, v (A)⟩\}$
127	110 120 126	3eqtr4d	$⊢ (((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \land (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v)) \to u = v$
128	127	ex	$⊢ ((φ \land u \in \{y \in D \| y (A) = 0\}) \land v \in \{y \in D \| y (A) = 0\}) \to ((x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v) \to u = v)$
129	128	anasss	$⊢ (φ \land (u \in \{y \in D \| y (A) = 0\} \land v \in \{y \in D \| y (A) = 0\})) \to ((x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v) \to u = v)$
130	129	ralrimivva	$⊢ φ \to \forall u \in \{y \in D \| y (A) = 0\} \forall v \in \{y \in D \| y (A) = 0\} ((x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v) \to u = v)$
131		dff13	$⊢ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} \underset{1-1}{⟶} {ℕ_{0}}^{J} \leftrightarrow ((x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} ⟶ {ℕ_{0}}^{J} \land \forall u \in \{y \in D \| y (A) = 0\} \forall v \in \{y \in D \| y (A) = 0\} ((x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (u) = (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) (v) \to u = v))$
132	85 130 131	sylanbrc	$⊢ φ \to (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} \underset{1-1}{⟶} {ℕ_{0}}^{J}$
133		df-f1	$⊢ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} \underset{1-1}{⟶} {ℕ_{0}}^{J} \leftrightarrow ((x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} ⟶ {ℕ_{0}}^{J} \land Fun {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1})$
134	133	simprbi	$⊢ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J}) : \{y \in D \| y (A) = 0\} \underset{1-1}{⟶} {ℕ_{0}}^{J} \to Fun {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1}$
135	132 134	syl	$⊢ φ \to Fun {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1}$
136	49 7 2 9	mplelsfi	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
137	136	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
138		imafi	$⊢ (Fun {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1} \land F supp \underset{˙}{0} \in Fin) \to {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1} [F supp \underset{˙}{0}] \in Fin$
139	135 137 138	syl2anc	$⊢ φ \to {(x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})}^{-1} [F supp \underset{˙}{0}] \in Fin$
140	84 139	eqeltrd	$⊢ φ \to (F \circ (x \in \{y \in D \| y (A) = 0\} ⟼ {x ↾}_{J})) supp \underset{˙}{0} \in Fin$
141	81 140	eqeltrrd	$⊢ φ \to (x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J})) supp \underset{˙}{0} \in Fin$
142		fconstmpt	$⊢ (D ∖ \{y \in D \| y (A) = 0\}) \times \{\underset{˙}{0}\} = (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0})$
143	142	oveq1i	$⊢ ((D ∖ \{y \in D \| y (A) = 0\}) \times \{\underset{˙}{0}\}) supp \underset{˙}{0} = (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}) supp \underset{˙}{0}$
144		fczsupp0	$⊢ ((D ∖ \{y \in D \| y (A) = 0\}) \times \{\underset{˙}{0}\}) supp \underset{˙}{0} = \emptyset$
145	143 144	eqtr3i	$⊢ (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}) supp \underset{˙}{0} = \emptyset$
146		0fi	$⊢ \emptyset \in Fin$
147	145 146	eqeltri	$⊢ (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}) supp \underset{˙}{0} \in Fin$
148	147	a1i	$⊢ φ \to (x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0}) supp \underset{˙}{0} \in Fin$
149	141 148	unfid	$⊢ φ \to {supp}_{\underset{˙}{0}} ((x \in \{y \in D \| y (A) = 0\} ⟼ F ({x ↾}_{J}))) \cup {supp}_{\underset{˙}{0}} ((x \in (D ∖ \{y \in D \| y (A) = 0\}) ⟼ \underset{˙}{0})) \in Fin$
150	48 149	eqeltrd	$⊢ φ \to (x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})) supp \underset{˙}{0} \in Fin$
151	34 35 37 150	isfsuppd	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in D ⟼ if (x (A) = 0, F ({x ↾}_{J}), \underset{˙}{0})))$
152	20 151	eqbrtrd	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) with typecode \|-
153		eqid	$⊢ I mPoly R = I mPoly R$
154	153 29 31 2 10	mplelbas	Could not format ( ( ( ( I extendVars R ) ` A ) ` F ) e. N <-> ( ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) ) : No typesetting found for \|- ( ( ( ( I extendVars R ) ` A ) ` F ) e. N <-> ( ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) ) with typecode \|-
155	33 152 154	sylanbrc	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N ) with typecode \|-

Metamath Proof Explorer

Theorem extvfvcl

Proof