extvfvcl - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > extvfvcl		Structured version Visualization version GIF version

Theorem extvfvcl 34150

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

**Hypotheses**
Ref	Expression
extvfvvcl.d	⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
extvfvvcl.3	⊢ 0 = (0_g‘𝑅)
extvfvvcl.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
extvfvvcl.r	⊢ (𝜑 → 𝑅 ∈ Ring)
extvfvvcl.b	⊢ 𝐵 = (Base‘𝑅)
extvfvvcl.j	⊢ 𝐽 = (𝐼 ∖ {𝐴})
extvfvvcl.m	⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))
extvfvvcl.1	⊢ (𝜑 → 𝐴 ∈ 𝐼)
extvfvvcl.f	⊢ (𝜑 → 𝐹 ∈ 𝑀)
extvfvcl.n	⊢ 𝑁 = (Base‘(𝐼 mPoly 𝑅))

**Assertion**
Ref	Expression
extvfvcl	⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ 𝑁)

Distinct variable groups: 𝐴,ℎ ℎ,𝐼 ℎ,𝐽 Allowed substitution hints: 𝜑(ℎ) 𝐵(ℎ) 𝐷(ℎ) 𝑅(ℎ) 𝐹(ℎ) 𝑀(ℎ) 𝑁(ℎ) 𝑉(ℎ) 0 (ℎ)

Proof of Theorem extvfvcl Dummy variables 𝑥 𝑦 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		extvfvvcl.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
2	1	fvexi 6891	. . . . 5 ⊢ 𝐵 ∈ V
3	2	a1i 11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
4		extvfvvcl.d	. . . . . 6 ⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
5		ovex 7445	. . . . . 6 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
6	4, 5	rabex2 5302	. . . . 5 ⊢ 𝐷 ∈ V
7	6	a1i 11	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
8		fvexd 6892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ↾ 𝐽)) ∈ V)
9		extvfvvcl.3	. . . . . . . 8 ⊢ 0 = (0_g‘𝑅)
10	9	fvexi 6891	. . . . . . 7 ⊢ 0 ∈ V
11	10	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 0 ∈ V)
12	8, 11	ifcld 4529	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 ) ∈ V)
13		extvfvvcl.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
14		extvfvvcl.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
15		extvfvvcl.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝐼)
16		extvfvvcl.j	. . . . . 6 ⊢ 𝐽 = (𝐼 ∖ {𝐴})
17		extvfvvcl.m	. . . . . 6 ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))
18		extvfvvcl.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑀)
19	4, 9, 13, 14, 15, 16, 17, 18	extvfv 34147	. . . . 5 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) = (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )))
20	13	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐼 ∈ 𝑉)
21	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑅 ∈ Ring)
22	15	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝐼)
23	18	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐹 ∈ 𝑀)
24		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
25	4, 9, 20, 21, 1, 16, 17, 22, 23, 24	extvfvvcl 34149	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((((𝐼extendVars𝑅)‘𝐴)‘𝐹)‘𝑥) ∈ 𝐵)
26	12, 19, 25	fmpt2d 7117	. . . 4 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹):𝐷⟶𝐵)
27	3, 7, 26	elmapdd 8845	. . 3 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ (𝐵 ↑_m 𝐷))
28		eqid 2761	. . . 4 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
29	4	psrbasfsupp 34125	. . . 4 ⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
30		eqid 2761	. . . 4 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
31	28, 1, 29, 30, 13	psrbas 22222	. . 3 ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (𝐵 ↑_m 𝐷))
32	27, 31	eleqtrrd 2864	. 2 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ (Base‘(𝐼 mPwSer 𝑅)))
33	7	mptexd 7222	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )) ∈ V)
34	10	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ V)
35	12	fmpttd 7107	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )):𝐷⟶V)
36	35	ffund 6706	. . . 4 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )))
37		fveq1 6876	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑦‘𝐴) = (𝑥‘𝐴))
38	37	eqeq1d 2763	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝐴) = 0 ↔ (𝑥‘𝐴) = 0))
39	38	cbvrabv 3423	. . . . . . . 8 ⊢ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} = {𝑥 ∈ 𝐷 ∣ (𝑥‘𝐴) = 0}
40	39	partfun2 33252	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ))
41	40	oveq1i 7422	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )) supp 0 ) = (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 )) supp 0 )
42	39, 7	rabexd 5301	. . . . . . . 8 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ∈ V)
43	42	mptexd 7222	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) ∈ V)
44	7	difexd 5293	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∈ V)
45	44	mptexd 7222	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) ∈ V)
46	43, 45, 34	suppun2 33259	. . . . . 6 ⊢ (𝜑 → (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 )) supp 0 ) = (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) supp 0 ) ∪ ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 )))
47	41, 46	eqtrid 2808	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )) supp 0 ) = (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) supp 0 ) ∪ ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 )))
48		eqid 2761	. . . . . . . . . 10 ⊢ (𝐽 mPoly 𝑅) = (𝐽 mPoly 𝑅)
49		eqid 2761	. . . . . . . . . . 11 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}
50	49	psrbasfsupp 34125	. . . . . . . . . 10 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ (^◡ℎ “ ℕ) ∈ Fin}
51	48, 1, 17, 50, 18	mplelf 22285	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}⟶𝐵)
52		breq1 5106	. . . . . . . . . 10 ⊢ (ℎ = (𝑥 ↾ 𝐽) → (ℎ finSupp 0 ↔ (𝑥 ↾ 𝐽) finSupp 0))
53		ssrab2 4028	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ⊆ 𝐷
54		ssrab2 4028	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼)
55	54	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼))
56	4, 55	eqsstrid 3969	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ⊆ (ℕ₀ ↑_m 𝐼))
57	53, 56	sstrid 3942	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ⊆ (ℕ₀ ↑_m 𝐼))
58	57	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → 𝑥 ∈ (ℕ₀ ↑_m 𝐼))
59		difssd 4084	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 ∖ {𝐴}) ⊆ 𝐼)
60	16, 59	eqsstrid 3969	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
61	60	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → 𝐽 ⊆ 𝐼)
62	58, 61	elmapssresd 8879	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → (𝑥 ↾ 𝐽) ∈ (ℕ₀ ↑_m 𝐽))
63	53	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ⊆ 𝐷)
64	63	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → 𝑥 ∈ 𝐷)
65	29	psrbagfsupp 22207	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → 𝑥 finSupp 0)
66	64, 65	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → 𝑥 finSupp 0)
67		c0ex 11281	. . . . . . . . . . . 12 ⊢ 0 ∈ V
68	67	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → 0 ∈ V)
69	66, 68	fsuppres 9369	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → (𝑥 ↾ 𝐽) finSupp 0)
70	52, 62, 69	elrabd 3647	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → (𝑥 ↾ 𝐽) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0})
71	51, 70	cofmpt 7125	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))))
72	71	oveq1d 7427	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))) supp 0 ) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) supp 0 ))
73	42	mptexd 7222	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) ∈ V)
74		suppco 8207	. . . . . . . . 9 ⊢ ((𝐹 ∈ 𝑀 ∧ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) ∈ V) → ((𝐹 ∘ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))) supp 0 ) = (^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) “ (𝐹 supp 0 )))
75	18, 73, 74	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 ∘ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))) supp 0 ) = (^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) “ (𝐹 supp 0 )))
76	62	fmpttd 7107	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}⟶(ℕ₀ ↑_m 𝐽))
77		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣))
78		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))
79		reseq1 5964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑢 → (𝑥 ↾ 𝐽) = (𝑢 ↾ 𝐽))
80		simpllr 788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0})
81	80	resexd 6019	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑢 ↾ 𝐽) ∈ V)
82	78, 79, 80, 81	fvmptd3 7009	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = (𝑢 ↾ 𝐽))
83		reseq1 5964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → (𝑥 ↾ 𝐽) = (𝑣 ↾ 𝐽))
84		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0})
85	84	resexd 6019	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑣 ↾ 𝐽) ∈ V)
86	78, 83, 84, 85	fvmptd3 7009	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣) = (𝑣 ↾ 𝐽))
87	77, 82, 86	3eqtr3d 2804	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑢 ↾ 𝐽) = (𝑣 ↾ 𝐽))
88	16	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝐽 = (𝐼 ∖ {𝐴}))
89	88	reseq2d 5970	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑢 ↾ 𝐽) = (𝑢 ↾ (𝐼 ∖ {𝐴})))
90	88	reseq2d 5970	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑣 ↾ 𝐽) = (𝑣 ↾ (𝐼 ∖ {𝐴})))
91	87, 89, 90	3eqtr3d 2804	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑢 ↾ (𝐼 ∖ {𝐴})) = (𝑣 ↾ (𝐼 ∖ {𝐴})))
92		fveq1 6876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑢 → (𝑦‘𝐴) = (𝑢‘𝐴))
93	92	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑢 → ((𝑦‘𝐴) = 0 ↔ (𝑢‘𝐴) = 0))
94	93, 80	elrabrd 3648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑢‘𝐴) = 0)
95		fveq1 6876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑣 → (𝑦‘𝐴) = (𝑣‘𝐴))
96	95	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → ((𝑦‘𝐴) = 0 ↔ (𝑣‘𝐴) = 0))
97	96, 84	elrabrd 3648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑣‘𝐴) = 0)
98	94, 97	eqtr4d 2799	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → (𝑢‘𝐴) = (𝑣‘𝐴))
99	98	opeq2d 4840	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → ⟨𝐴, (𝑢‘𝐴)⟩ = ⟨𝐴, (𝑣‘𝐴)⟩)
100	99	sneqd 4596	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → {⟨𝐴, (𝑢‘𝐴)⟩} = {⟨𝐴, (𝑣‘𝐴)⟩})
101	91, 100	uneq12d 4116	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → ((𝑢 ↾ (𝐼 ∖ {𝐴})) ∪ {⟨𝐴, (𝑢‘𝐴)⟩}) = ((𝑣 ↾ (𝐼 ∖ {𝐴})) ∪ {⟨𝐴, (𝑣‘𝐴)⟩}))
102	56	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝐷 ⊆ (ℕ₀ ↑_m 𝐼))
103	53, 80	sselid 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢 ∈ 𝐷)
104	102, 103	sseldd 3932	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢 ∈ (ℕ₀ ↑_m 𝐼))
105	104	elmaprd 8854	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢:𝐼⟶ℕ₀)
106	105	ffnd 6702	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢 Fn 𝐼)
107	15	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝐴 ∈ 𝐼)
108		fnsnsplit 7181	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 Fn 𝐼 ∧ 𝐴 ∈ 𝐼) → 𝑢 = ((𝑢 ↾ (𝐼 ∖ {𝐴})) ∪ {⟨𝐴, (𝑢‘𝐴)⟩}))
109	106, 107, 108	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢 = ((𝑢 ↾ (𝐼 ∖ {𝐴})) ∪ {⟨𝐴, (𝑢‘𝐴)⟩}))
110	53, 84	sselid 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑣 ∈ 𝐷)
111	102, 110	sseldd 3932	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑣 ∈ (ℕ₀ ↑_m 𝐼))
112	111	elmaprd 8854	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑣:𝐼⟶ℕ₀)
113	112	ffnd 6702	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑣 Fn 𝐼)
114		fnsnsplit 7181	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 Fn 𝐼 ∧ 𝐴 ∈ 𝐼) → 𝑣 = ((𝑣 ↾ (𝐼 ∖ {𝐴})) ∪ {⟨𝐴, (𝑣‘𝐴)⟩}))
115	113, 107, 114	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑣 = ((𝑣 ↾ (𝐼 ∖ {𝐴})) ∪ {⟨𝐴, (𝑣‘𝐴)⟩}))
116	101, 109, 115	3eqtr4d 2806	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣)) → 𝑢 = 𝑣)
117	116	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) → (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣) → 𝑢 = 𝑣))
118	117	anasss 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ∧ 𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0})) → (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣) → 𝑢 = 𝑣))
119	118	ralrimivva 3206	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}∀𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣) → 𝑢 = 𝑣))
120		dff13 7250	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}–1-1→(ℕ₀ ↑_m 𝐽) ↔ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}⟶(ℕ₀ ↑_m 𝐽) ∧ ∀𝑢 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}∀𝑣 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑢) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))‘𝑣) → 𝑢 = 𝑣)))
121	76, 119, 120	sylanbrc 595	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}–1-1→(ℕ₀ ↑_m 𝐽))
122		df-f1 6536	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}–1-1→(ℕ₀ ↑_m 𝐽) ↔ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}⟶(ℕ₀ ↑_m 𝐽) ∧ Fun ^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))))
123	122	simprbi 503	. . . . . . . . . 10 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)):{𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}–1-1→(ℕ₀ ↑_m 𝐽) → Fun ^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)))
124	121, 123	syl 18	. . . . . . . . 9 ⊢ (𝜑 → Fun ^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)))
125	48, 17, 9, 18	mplelsfi 22282	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 finSupp 0 )
126	125	fsuppimpd 9345	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)
127		imafi 9291	. . . . . . . . 9 ⊢ ((Fun ^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) ∧ (𝐹 supp 0 ) ∈ Fin) → (^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) “ (𝐹 supp 0 )) ∈ Fin)
128	124, 126, 127	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (^◡(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽)) “ (𝐹 supp 0 )) ∈ Fin)
129	75, 128	eqeltrd 2861	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝑥 ↾ 𝐽))) supp 0 ) ∈ Fin)
130	72, 129	eqeltrrd 2862	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) supp 0 ) ∈ Fin)
131		fconstmpt 5713	. . . . . . . . . 10 ⊢ ((𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) × { 0 }) = (𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 )
132	131	oveq1i 7422	. . . . . . . . 9 ⊢ (((𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) × { 0 }) supp 0 ) = ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 )
133		fczsupp0 8194	. . . . . . . . 9 ⊢ (((𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) × { 0 }) supp 0 ) = ∅
134	132, 133	eqtr3i 2786	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 ) = ∅
135		0fi 9054	. . . . . . . 8 ⊢ ∅ ∈ Fin
136	134, 135	eqeltri 2857	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 ) ∈ Fin
137	136	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 ) ∈ Fin)
138	130, 137	unfid 9171	. . . . 5 ⊢ (𝜑 → (((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0} ↦ (𝐹‘(𝑥 ↾ 𝐽))) supp 0 ) ∪ ((𝑥 ∈ (𝐷 ∖ {𝑦 ∈ 𝐷 ∣ (𝑦‘𝐴) = 0}) ↦ 0 ) supp 0 )) ∈ Fin)
139	47, 138	eqeltrd 2861	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )) supp 0 ) ∈ Fin)
140	33, 34, 36, 139	isfsuppd 9342	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )) finSupp 0 )
141	19, 140	eqbrtrd 5127	. 2 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) finSupp 0 )
142		eqid 2761	. . 3 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
143		extvfvcl.n	. . 3 ⊢ 𝑁 = (Base‘(𝐼 mPoly 𝑅))
144	142, 28, 30, 9, 143	mplelbas 22278	. 2 ⊢ ((((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ 𝑁 ↔ ((((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (((𝐼extendVars𝑅)‘𝐴)‘𝐹) finSupp 0 ))
145	32, 141, 144	sylanbrc 595	1 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ 𝑁)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 ifcif 4482 {csn 4584 ⟨cop 4590 class class class wbr 5103 ↦ cmpt 5186 × cxp 5649 ^◡ccnv 5650 ↾ cres 5653 “ cima 5654 ∘ ccom 5655 Fun wfun 6525 Fn wfn 6526 ⟶wf 6527 –1-1→wf1 6528 ‘cfv 6531 (class class class)co 7412 supp csupp 8161 ↑_m cmap 8831 Fincfn 8957 finSupp cfsupp 9337 0cc0 11181 ℕ₀cn0 12587 Basecbs 17367 0_gc0g 17590 Ringcrg 20439 mPwSer cmps 22192 mPoly cmpl 22194 extendVarscextv 34143

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9338 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-z 12675 df-uz 12947 df-fz 13621 df-struct 17305 df-sets 17322 df-slot 17340 df-ndx 17352 df-base 17368 df-ress 17389 df-plusg 17421 df-mulr 17422 df-sca 17424 df-vsca 17425 df-tset 17427 df-0g 17592 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-grp 19127 df-ring 20441 df-psr 22197 df-mpl 22199 df-extv 34144

This theorem is used by: extvfvalf 34151 evlextv 34156 esplyindfv 34190

W3C validator