Metamath Proof Explorer

Theorem 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 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
extvfvvcl.3 ⊢ 0 = ( 0g ‘ 𝑅 )
extvfvvcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
extvfvvcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
extvfvvcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
extvfvvcl.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
extvfvvcl.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
extvfvvcl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
extvfvvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
extvfvcl.n ⊢ 𝑁 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion extvfvcl ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ 𝑁 )

Proof

Step Hyp Ref Expression
1 extvfvvcl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 extvfvvcl.3 ⊢ 0 = ( 0g ‘ 𝑅 )
3 extvfvvcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 extvfvvcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 extvfvvcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 extvfvvcl.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
7 extvfvvcl.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
8 extvfvvcl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
9 extvfvvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
10 extvfvcl.n ⊢ 𝑁 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
11 5 fvexi ⊢ 𝐵 ∈ V
12 11 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
13 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
14 1 13 rabex2 ⊢ 𝐷 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
16 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ∈ V )
17 2 fvexi ⊢ 0 ∈ V
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 0 ∈ V )
19 16 18 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ∈ V )
20 1 2 3 4 8 6 7 9 extvfv ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
21 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
22 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑅 ∈ Ring )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝐼 )
24 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐹 ∈ 𝑀 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
26 1 2 21 22 5 6 7 23 24 25 extvfvvcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 )
27 19 20 26 fmpt2d ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) : 𝐷 ⟶ 𝐵 )
28 12 15 27 elmapdd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ ( 𝐵 ↑m 𝐷 ) )
29 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
30 1 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
31 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
32 29 5 30 31 3 psrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐵 ↑m 𝐷 ) )
33 28 32 eleqtrrd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
34 15 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ∈ V )
35 17 a1i ⊢ ( 𝜑 → 0 ∈ V )
36 19 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) : 𝐷 ⟶ V )
37 36 ffund ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
38 fveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ‘ 𝐴 ) = ( 𝑥 ‘ 𝐴 ) )
39 38 eqeq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ‘ 𝐴 ) = 0 ↔ ( 𝑥 ‘ 𝐴 ) = 0 ) )
40 39 cbvrabv ⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } = { 𝑥 ∈ 𝐷 ∣ ( 𝑥 ‘ 𝐴 ) = 0 }
41 40 partfun2 ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) )
42 41 oveq1i ⊢ ( ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) supp 0 ) = ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) ) supp 0 )
43 40 15 rabexd ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∈ V )
44 43 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∈ V )
45 15 difexd ⊢ ( 𝜑 → ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∈ V )
46 45 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) ∈ V )
47 44 46 35 suppun2 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) ) supp 0 ) = ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∪ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ) )
48 42 47 eqtrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) supp 0 ) = ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∪ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ) )
49 eqid ⊢ ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
50 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
51 50 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
52 49 5 7 51 9 mplelf ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ⟶ 𝐵 )
53 breq1 ⊢ ( ℎ = ( 𝑥 ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( 𝑥 ↾ 𝐽 ) finSupp 0 ) )
54 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⊆ 𝐷
55 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
56 55 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
57 1 56 eqsstrid ⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
58 54 57 sstrid ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
59 58 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) )
60 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝐴 } ) ⊆ 𝐼 )
61 6 60 eqsstrid ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝐽 ⊆ 𝐼 )
63 59 62 elmapssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
64 54 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⊆ 𝐷 )
65 64 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 ∈ 𝐷 )
66 30 psrbagfsupp ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 finSupp 0 )
67 65 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 finSupp 0 )
68 c0ex ⊢ 0 ∈ V
69 68 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 0 ∈ V )
70 67 69 fsuppres ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) finSupp 0 )
71 53 63 70 elrabd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
72 52 71 cofmpt ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) )
73 72 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) )
74 43 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ∈ V )
75 suppco ⊢ ( ( 𝐹 ∈ 𝑀 ∧ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ∈ V ) → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) = ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) )
76 9 74 75 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) = ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) )
77 63 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⟶ ( ℕ0 ↑m 𝐽 ) )
78 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) )
79 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) )
80 reseq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ↾ 𝐽 ) = ( 𝑢 ↾ 𝐽 ) )
81 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } )
82 81 resexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ 𝐽 ) ∈ V )
83 79 80 81 82 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( 𝑢 ↾ 𝐽 ) )
84 reseq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 ↾ 𝐽 ) = ( 𝑣 ↾ 𝐽 ) )
85 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } )
86 85 resexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑣 ↾ 𝐽 ) ∈ V )
87 79 84 85 86 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) = ( 𝑣 ↾ 𝐽 ) )
88 78 83 87 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ 𝐽 ) = ( 𝑣 ↾ 𝐽 ) )
89 6 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐽 = ( 𝐼 ∖ { 𝐴 } ) )
90 89 reseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ 𝐽 ) = ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) )
91 89 reseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑣 ↾ 𝐽 ) = ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) )
92 88 90 91 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) = ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) )
93 fveq1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 ‘ 𝐴 ) = ( 𝑢 ‘ 𝐴 ) )
94 93 eqeq1d ⊢ ( 𝑦 = 𝑢 → ( ( 𝑦 ‘ 𝐴 ) = 0 ↔ ( 𝑢 ‘ 𝐴 ) = 0 ) )
95 94 81 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ‘ 𝐴 ) = 0 )
96 fveq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ‘ 𝐴 ) = ( 𝑣 ‘ 𝐴 ) )
97 96 eqeq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑦 ‘ 𝐴 ) = 0 ↔ ( 𝑣 ‘ 𝐴 ) = 0 ) )
98 97 85 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑣 ‘ 𝐴 ) = 0 )
99 95 98 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ‘ 𝐴 ) = ( 𝑣 ‘ 𝐴 ) )
100 99 opeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ = ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ )
101 100 sneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } = { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } )
102 92 101 uneq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } ) = ( ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } ) )
103 57 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
104 54 81 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 ∈ 𝐷 )
105 103 104 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 ∈ ( ℕ0 ↑m 𝐼 ) )
106 105 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 : 𝐼 ⟶ ℕ0 )
107 106 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 Fn 𝐼 )
108 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐴 ∈ 𝐼 )
109 fnsnsplit ⊢ ( ( 𝑢 Fn 𝐼 ∧ 𝐴 ∈ 𝐼 ) → 𝑢 = ( ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } ) )
110 107 108 109 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 = ( ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } ) )
111 54 85 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 ∈ 𝐷 )
112 103 111 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 ∈ ( ℕ0 ↑m 𝐼 ) )
113 112 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 : 𝐼 ⟶ ℕ0 )
114 113 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 Fn 𝐼 )
115 fnsnsplit ⊢ ( ( 𝑣 Fn 𝐼 ∧ 𝐴 ∈ 𝐼 ) → 𝑣 = ( ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } ) )
116 114 108 115 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 = ( ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } ) )
117 102 110 116 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 = 𝑣 )
118 117 ex ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
119 118 anasss ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ) → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
120 119 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∀ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
121 dff13 ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) ↔ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⟶ ( ℕ0 ↑m 𝐽 ) ∧ ∀ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∀ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
122 77 120 121 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) )
123 df-f1 ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) ↔ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⟶ ( ℕ0 ↑m 𝐽 ) ∧ Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) )
124 123 simprbi ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) → Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) )
125 122 124 syl ⊢ ( 𝜑 → Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) )
126 49 7 2 9 mplelsfi ⊢ ( 𝜑 → 𝐹 finSupp 0 )
127 126 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
128 imafi ⊢ ( ( Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) ∈ Fin )
129 125 127 128 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) ∈ Fin )
130 76 129 eqeltrd ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∈ Fin )
131 73 130 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∈ Fin )
132 fconstmpt ⊢ ( ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) × { 0 } ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 )
133 132 oveq1i ⊢ ( ( ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) × { 0 } ) supp 0 ) = ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 )
134 fczsupp0 ⊢ ( ( ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) × { 0 } ) supp 0 ) = ∅
135 133 134 eqtr3i ⊢ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) = ∅
136 0fi ⊢ ∅ ∈ Fin
137 135 136 eqeltri ⊢ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ∈ Fin
138 137 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ∈ Fin )
139 131 138 unfid ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∪ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ) ∈ Fin )
140 48 139 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) supp 0 ) ∈ Fin )
141 34 35 37 140 isfsuppd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) finSupp 0 )
142 20 141 eqbrtrd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) finSupp 0 )
143 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
144 143 29 31 2 10 mplelbas ⊢ ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ 𝑁 ↔ ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) finSupp 0 ) )
145 33 142 144 sylanbrc ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ 𝑁 )