This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem esplyind

Description: A recursive formula for the elementary symmetric polynomials. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses esplyind.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
esplyind.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
esplyind.p ⊢ + = ( +g ‘ 𝑊 )
esplyind.m ⊢ · = ( .r ‘ 𝑊 )
esplyind.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplyind.g ⊢ 𝐺 = ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 )
esplyind.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyind.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplyind.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
esplyind.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
esplyind.e ⊢ 𝐸 = ( 𝐽 eSymPoly 𝑅 )
esplyind.k ⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... ( ♯ ‘ 𝐼 ) ) )
esplyind.1 ⊢ 𝐶 = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
Assertion esplyind ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) + ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 esplyind.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
2 esplyind.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3 esplyind.p ⊢ + = ( +g ‘ 𝑊 )
4 esplyind.m ⊢ · = ( .r ‘ 𝑊 )
5 esplyind.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6 esplyind.g ⊢ 𝐺 = ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 )
7 esplyind.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
8 esplyind.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 esplyind.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
10 esplyind.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
11 esplyind.e ⊢ 𝐸 = ( 𝐽 eSymPoly 𝑅 )
12 esplyind.k ⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... ( ♯ ‘ 𝐼 ) ) )
13 esplyind.1 ⊢ 𝐶 = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
14 ovif12 ⊢ ( if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ( +g ‘ 𝑅 ) if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) , ( ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
17 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18 8 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑅 ∈ Grp )
20 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
21 15 20 8 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
23 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
24 15 17 grpidcl ⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
25 8 23 24 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27 22 26 ifcld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
29 15 16 17 19 28 grplidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
30 snsspr1 ⊢ { 0 } ⊆ { 0 , 1 }
31 30 biantru ⊢ ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ↔ ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ { 0 } ⊆ { 0 , 1 } ) )
32 unss ⊢ ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ { 0 } ⊆ { 0 , 1 } ) ↔ ( ran ( 𝑓 ↾ 𝐽 ) ∪ { 0 } ) ⊆ { 0 , 1 } )
33 31 32 bitri ⊢ ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ↔ ( ran ( 𝑓 ↾ 𝐽 ) ∪ { 0 } ) ⊆ { 0 , 1 } )
34 7 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝐼 ∈ Fin )
35 nn0ex ⊢ ℕ0 ∈ V
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ℕ0 ∈ V )
37 5 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
38 37 a1i ⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
39 38 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) )
40 34 36 39 elmaprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
41 40 freld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → Rel 𝑓 )
42 40 ffnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 Fn 𝐼 )
43 42 fndmd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → dom 𝑓 = 𝐼 )
44 10 uneq1i ⊢ ( 𝐽 ∪ { 𝑌 } ) = ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } )
45 9 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝐼 )
46 undifr ⊢ ( { 𝑌 } ⊆ 𝐼 ↔ ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
47 45 46 sylib ⊢ ( 𝜑 → ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
48 44 47 eqtr2id ⊢ ( 𝜑 → 𝐼 = ( 𝐽 ∪ { 𝑌 } ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝐼 = ( 𝐽 ∪ { 𝑌 } ) )
50 43 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → dom 𝑓 = ( 𝐽 ∪ { 𝑌 } ) )
51 10 ineq1i ⊢ ( 𝐽 ∩ { 𝑌 } ) = ( ( 𝐼 ∖ { 𝑌 } ) ∩ { 𝑌 } )
52 disjdifr ⊢ ( ( 𝐼 ∖ { 𝑌 } ) ∩ { 𝑌 } ) = ∅
53 51 52 eqtri ⊢ ( 𝐽 ∩ { 𝑌 } ) = ∅
54 53 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝐽 ∩ { 𝑌 } ) = ∅ )
55 reldisjun ⊢ ( ( Rel 𝑓 ∧ dom 𝑓 = ( 𝐽 ∪ { 𝑌 } ) ∧ ( 𝐽 ∩ { 𝑌 } ) = ∅ ) → 𝑓 = ( ( 𝑓 ↾ 𝐽 ) ∪ ( 𝑓 ↾ { 𝑌 } ) ) )
56 41 50 54 55 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 = ( ( 𝑓 ↾ 𝐽 ) ∪ ( 𝑓 ↾ { 𝑌 } ) ) )
57 56 rneqd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ran 𝑓 = ran ( ( 𝑓 ↾ 𝐽 ) ∪ ( 𝑓 ↾ { 𝑌 } ) ) )
58 rnun ⊢ ran ( ( 𝑓 ↾ 𝐽 ) ∪ ( 𝑓 ↾ { 𝑌 } ) ) = ( ran ( 𝑓 ↾ 𝐽 ) ∪ ran ( 𝑓 ↾ { 𝑌 } ) )
59 57 58 eqtr2di ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ran ( 𝑓 ↾ 𝐽 ) ∪ ran ( 𝑓 ↾ { 𝑌 } ) ) = ran 𝑓 )
60 42 fnfund ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → Fun 𝑓 )
61 9 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑌 ∈ 𝐼 )
62 61 43 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑌 ∈ dom 𝑓 )
63 rnressnsn ⊢ ( ( Fun 𝑓 ∧ 𝑌 ∈ dom 𝑓 ) → ran ( 𝑓 ↾ { 𝑌 } ) = { ( 𝑓 ‘ 𝑌 ) } )
64 60 62 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ran ( 𝑓 ↾ { 𝑌 } ) = { ( 𝑓 ‘ 𝑌 ) } )
65 64 uneq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ran ( 𝑓 ↾ 𝐽 ) ∪ ran ( 𝑓 ↾ { 𝑌 } ) ) = ( ran ( 𝑓 ↾ 𝐽 ) ∪ { ( 𝑓 ‘ 𝑌 ) } ) )
66 59 65 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ran 𝑓 = ( ran ( 𝑓 ↾ 𝐽 ) ∪ { ( 𝑓 ‘ 𝑌 ) } ) )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ran 𝑓 = ( ran ( 𝑓 ↾ 𝐽 ) ∪ { ( 𝑓 ‘ 𝑌 ) } ) )
68 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ‘ 𝑌 ) = 0 )
69 68 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → { ( 𝑓 ‘ 𝑌 ) } = { 0 } )
70 69 uneq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ran ( 𝑓 ↾ 𝐽 ) ∪ { ( 𝑓 ‘ 𝑌 ) } ) = ( ran ( 𝑓 ↾ 𝐽 ) ∪ { 0 } ) )
71 67 70 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ran 𝑓 = ( ran ( 𝑓 ↾ 𝐽 ) ∪ { 0 } ) )
72 71 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ran 𝑓 ⊆ { 0 , 1 } ↔ ( ran ( 𝑓 ↾ 𝐽 ) ∪ { 0 } ) ⊆ { 0 , 1 } ) )
73 33 72 bitr4id ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ↔ ran 𝑓 ⊆ { 0 , 1 } ) )
74 56 oveq1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) = ( ( ( 𝑓 ↾ 𝐽 ) ∪ ( 𝑓 ↾ { 𝑌 } ) ) supp 0 ) )
75 39 resexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ↾ 𝐽 ) ∈ V )
76 39 resexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ↾ { 𝑌 } ) ∈ V )
77 0nn0 ⊢ 0 ∈ ℕ0
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 0 ∈ ℕ0 )
79 75 76 78 suppun2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ( ( 𝑓 ↾ 𝐽 ) ∪ ( 𝑓 ↾ { 𝑌 } ) ) supp 0 ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) )
80 74 79 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 supp 0 ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) )
82 fnressn ⊢ ( ( 𝑓 Fn 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑓 ↾ { 𝑌 } ) = { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ } )
83 42 61 82 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ↾ { 𝑌 } ) = { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ } )
84 83 oveq1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) = ( { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ } supp 0 ) )
85 40 61 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ‘ 𝑌 ) ∈ ℕ0 )
86 eqid ⊢ { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ } = { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ }
87 86 suppsnop ⊢ ( ( 𝑌 ∈ 𝐼 ∧ ( 𝑓 ‘ 𝑌 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ } supp 0 ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) )
88 61 85 78 87 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( { ⟨ 𝑌 , ( 𝑓 ‘ 𝑌 ) ⟩ } supp 0 ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) )
89 84 88 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) )
90 89 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) )
91 68 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) = ∅ )
92 90 91 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) = ∅ )
93 92 uneq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ∅ ) )
94 un0 ⊢ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ∅ ) = ( ( 𝑓 ↾ 𝐽 ) supp 0 )
95 93 94 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) = ( ( 𝑓 ↾ 𝐽 ) supp 0 ) )
96 81 95 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ 𝐽 ) supp 0 ) = ( 𝑓 supp 0 ) )
97 96 fveqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ↔ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) )
98 73 97 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) ↔ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) ) )
99 98 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
100 29 99 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
101 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑅 ∈ Grp )
102 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
103 5 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
104 6 fveq1i ⊢ ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) = ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) )
105 eqid ⊢ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
106 1 fveq2i ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
107 5 17 7 8 15 10 105 9 106 extvfvalf ⊢ ( 𝜑 → ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) : ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) ⟶ ( Base ‘ 𝑊 ) )
108 11 fveq1i ⊢ ( 𝐸 ‘ ( 𝐾 − 1 ) ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 − 1 ) )
109 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑌 } ) ⊆ 𝐼 )
110 10 109 eqsstrid ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
111 7 110 ssfid ⊢ ( 𝜑 → 𝐽 ∈ Fin )
112 elfznn ⊢ ( 𝐾 ∈ ( 1 ... ( ♯ ‘ 𝐼 ) ) → 𝐾 ∈ ℕ )
113 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
114 12 112 113 3syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
115 13 111 8 114 105 esplympl ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 − 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
116 108 115 eqeltrid ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝐾 − 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
117 107 116 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ∈ ( Base ‘ 𝑊 ) )
118 104 117 eqeltrid ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ∈ ( Base ‘ 𝑊 ) )
119 1 15 102 103 118 mplelf ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
120 119 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
121 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑓 ∈ 𝐷 )
122 indf ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑌 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ { 0 , 1 } )
123 7 45 122 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ { 0 , 1 } )
124 77 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
125 1nn0 ⊢ 1 ∈ ℕ0
126 125 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
127 124 126 prssd ⊢ ( 𝜑 → { 0 , 1 } ⊆ ℕ0 )
128 123 127 fssd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ ℕ0 )
129 128 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ ℕ0 )
130 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝐼 ∈ Fin )
131 130 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → 𝐼 ∈ Fin )
132 45 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → { 𝑌 } ⊆ 𝐼 )
133 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → 𝑥 = 𝑌 )
134 velsn ⊢ ( 𝑥 ∈ { 𝑌 } ↔ 𝑥 = 𝑌 )
135 133 134 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → 𝑥 ∈ { 𝑌 } )
136 ind1 ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑌 } ⊆ 𝐼 ∧ 𝑥 ∈ { 𝑌 } ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) = 1 )
137 131 132 135 136 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) = 1 )
138 40 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
139 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → 𝑥 ∈ 𝐼 )
140 138 139 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 )
141 133 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑌 ) )
142 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ¬ ( 𝑓 ‘ 𝑌 ) = 0 )
143 142 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( 𝑓 ‘ 𝑌 ) ≠ 0 )
144 141 143 eqnetrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( 𝑓 ‘ 𝑥 ) ≠ 0 )
145 elnnne0 ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ℕ ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
146 140 144 145 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ )
147 146 nnge1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → 1 ≤ ( 𝑓 ‘ 𝑥 ) )
148 137 147 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 = 𝑌 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) )
149 130 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → 𝐼 ∈ Fin )
150 45 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → { 𝑌 } ⊆ 𝐼 )
151 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → 𝑥 ∈ 𝐼 )
152 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → 𝑥 ≠ 𝑌 )
153 151 152 eldifsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) )
154 ind0 ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑌 } ⊆ 𝐼 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) = 0 )
155 149 150 153 154 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) = 0 )
156 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
157 156 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 )
158 157 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 )
159 158 nn0ge0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → 0 ≤ ( 𝑓 ‘ 𝑥 ) )
160 155 159 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ≠ 𝑌 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) )
161 148 160 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) )
162 161 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ∀ 𝑥 ∈ 𝐼 ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) )
163 129 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 )
164 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑓 Fn 𝐼 )
165 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
166 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) )
167 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
168 163 164 130 130 165 166 167 ofrfval ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ∘r ≤ 𝑓 ↔ ∀ 𝑥 ∈ 𝐼 ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) ) )
169 162 168 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ∘r ≤ 𝑓 )
170 103 psrbagcon ⊢ ( ( 𝑓 ∈ 𝐷 ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ∘r ≤ 𝑓 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ 𝐷 ∧ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∘r ≤ 𝑓 ) )
171 170 simpld ⊢ ( ( 𝑓 ∈ 𝐷 ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ∘r ≤ 𝑓 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ 𝐷 )
172 121 129 169 171 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ 𝐷 )
173 120 172 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ∈ ( Base ‘ 𝑅 ) )
174 15 16 17 101 173 grpridd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) )
175 104 fveq1i ⊢ ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) = ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) )
176 175 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) = ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) )
177 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑅 ∈ Ring )
178 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑌 ∈ 𝐼 )
179 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝐸 ‘ ( 𝐾 − 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
180 5 17 130 177 178 10 105 179 172 extvfvv ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) = if ( ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 , ( ( 𝐸 ‘ ( 𝐾 − 1 ) ) ‘ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) )
181 13 111 8 114 17 20 esplyfval3 ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 − 1 ) ) = ( 𝑧 ∈ 𝐶 ↦ if ( ( ran 𝑧 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑧 supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
182 108 181 eqtrid ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝐾 − 1 ) ) = ( 𝑧 ∈ 𝐶 ↦ if ( ( ran 𝑧 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑧 supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
183 182 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝐸 ‘ ( 𝐾 − 1 ) ) = ( 𝑧 ∈ 𝐶 ↦ if ( ( ran 𝑧 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑧 supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
184 59 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ( ran ( 𝑓 ↾ 𝐽 ) ∪ ran ( 𝑓 ↾ { 𝑌 } ) ) = ran 𝑓 )
185 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) )
186 123 ffnd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 )
187 186 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 )
188 42 187 34 34 165 offn ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) Fn 𝐼 )
189 188 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) Fn 𝐼 )
190 110 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → 𝐽 ⊆ 𝐼 )
191 189 190 fnssresd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) Fn 𝐽 )
192 fneq1 ⊢ ( 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) → ( 𝑧 Fn 𝐽 ↔ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) Fn 𝐽 ) )
193 192 biimpar ⊢ ( ( 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) Fn 𝐽 ) → 𝑧 Fn 𝐽 )
194 185 191 193 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → 𝑧 Fn 𝐽 )
195 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 𝑓 Fn 𝐼 )
196 110 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 𝐽 ⊆ 𝐼 )
197 195 196 fnssresd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) Fn 𝐽 )
198 197 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( 𝑓 ↾ 𝐽 ) Fn 𝐽 )
199 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) )
200 199 fveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑧 ‘ 𝑥 ) = ( ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ‘ 𝑥 ) )
201 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
202 201 fvresd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ‘ 𝑥 ) = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑥 ) )
203 195 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑓 Fn 𝐼 )
204 163 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 )
205 204 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 )
206 34 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 𝐼 ∈ Fin )
207 206 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐼 ∈ Fin )
208 190 sselda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐼 )
209 fnfvof ⊢ ( ( ( 𝑓 Fn 𝐼 ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 ) ∧ ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ) )
210 203 205 207 208 209 syl22anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ) )
211 45 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → { 𝑌 } ⊆ 𝐼 )
212 201 10 eleqtrdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) )
213 207 211 212 154 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) = 0 )
214 213 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑓 ‘ 𝑥 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) − 0 ) )
215 156 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
216 215 208 ffvelcdmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 )
217 216 nn0cnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
218 217 subid1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑓 ‘ 𝑥 ) − 0 ) = ( 𝑓 ‘ 𝑥 ) )
219 201 fvresd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑓 ↾ 𝐽 ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
220 218 219 eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑓 ‘ 𝑥 ) − 0 ) = ( ( 𝑓 ↾ 𝐽 ) ‘ 𝑥 ) )
221 210 214 220 3eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑥 ) = ( ( 𝑓 ↾ 𝐽 ) ‘ 𝑥 ) )
222 200 202 221 3eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑧 ‘ 𝑥 ) = ( ( 𝑓 ↾ 𝐽 ) ‘ 𝑥 ) )
223 194 198 222 eqfnfvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → 𝑧 = ( 𝑓 ↾ 𝐽 ) )
224 223 rneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ran 𝑧 = ran ( 𝑓 ↾ 𝐽 ) )
225 224 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran 𝑧 = ran ( 𝑓 ↾ 𝐽 ) )
226 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran 𝑧 ⊆ { 0 , 1 } )
227 225 226 eqsstrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } )
228 60 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → Fun 𝑓 )
229 62 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → 𝑌 ∈ dom 𝑓 )
230 228 229 63 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran ( 𝑓 ↾ { 𝑌 } ) = { ( 𝑓 ‘ 𝑌 ) } )
231 85 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ‘ 𝑌 ) ∈ ℕ0 )
232 231 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ‘ 𝑌 ) ∈ ℂ )
233 123 9 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ∈ { 0 , 1 } )
234 127 233 sseldd ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ∈ ℕ0 )
235 234 nn0cnd ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ∈ ℂ )
236 235 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ∈ ℂ )
237 178 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 𝑌 ∈ 𝐼 )
238 fnfvof ⊢ ( ( ( 𝑓 Fn 𝐼 ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 ) ∧ ( 𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = ( ( 𝑓 ‘ 𝑌 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ) )
239 195 204 206 237 238 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = ( ( 𝑓 ‘ 𝑌 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ) )
240 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 )
241 239 240 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ‘ 𝑌 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ) = 0 )
242 232 236 241 subeq0d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ‘ 𝑌 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) )
243 snidg ⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ { 𝑌 } )
244 9 243 syl ⊢ ( 𝜑 → 𝑌 ∈ { 𝑌 } )
245 ind1 ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑌 } ⊆ 𝐼 ∧ 𝑌 ∈ { 𝑌 } ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) = 1 )
246 7 45 244 245 syl3anc ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) = 1 )
247 246 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) = 1 )
248 242 247 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ‘ 𝑌 ) = 1 )
249 248 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ( 𝑓 ‘ 𝑌 ) = 1 )
250 249 sneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → { ( 𝑓 ‘ 𝑌 ) } = { 1 } )
251 230 250 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran ( 𝑓 ↾ { 𝑌 } ) = { 1 } )
252 snsspr2 ⊢ { 1 } ⊆ { 0 , 1 }
253 251 252 eqsstrdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran ( 𝑓 ↾ { 𝑌 } ) ⊆ { 0 , 1 } )
254 227 253 unssd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ( ran ( 𝑓 ↾ 𝐽 ) ∪ ran ( 𝑓 ↾ { 𝑌 } ) ) ⊆ { 0 , 1 } )
255 184 254 eqsstrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑧 ⊆ { 0 , 1 } ) → ran 𝑓 ⊆ { 0 , 1 } )
256 223 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑧 = ( 𝑓 ↾ 𝐽 ) )
257 256 rneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran 𝑧 = ran ( 𝑓 ↾ 𝐽 ) )
258 rnresss ⊢ ran ( 𝑓 ↾ 𝐽 ) ⊆ ran 𝑓
259 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran 𝑓 ⊆ { 0 , 1 } )
260 258 259 sstrid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } )
261 257 260 eqsstrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran 𝑧 ⊆ { 0 , 1 } )
262 255 261 impbida ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( ran 𝑧 ⊆ { 0 , 1 } ↔ ran 𝑓 ⊆ { 0 , 1 } ) )
263 223 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( 𝑧 supp 0 ) = ( ( 𝑓 ↾ 𝐽 ) supp 0 ) )
264 263 fveqeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( ( ♯ ‘ ( 𝑧 supp 0 ) ) = ( 𝐾 − 1 ) ↔ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) )
265 262 264 anbi12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → ( ( ran 𝑧 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑧 supp 0 ) ) = ( 𝐾 − 1 ) ) ↔ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) ) )
266 265 ifbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ 𝑧 = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) → if ( ( ran 𝑧 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑧 supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
267 breq1 ⊢ ( ℎ = ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) finSupp 0 ) )
268 35 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ℕ0 ∈ V )
269 206 196 ssexd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 𝐽 ∈ V )
270 37 172 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ ( ℕ0 ↑m 𝐼 ) )
271 270 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ ( ℕ0 ↑m 𝐼 ) )
272 206 268 271 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) : 𝐼 ⟶ ℕ0 )
273 272 196 fssresd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
274 268 269 273 elmapdd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
275 breq1 ⊢ ( ℎ = ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) → ( ℎ finSupp 0 ↔ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) finSupp 0 ) )
276 172 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ 𝐷 )
277 276 5 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
278 275 277 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) finSupp 0 )
279 77 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 0 ∈ ℕ0 )
280 278 279 fsuppres ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) finSupp 0 )
281 267 274 280 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
282 281 13 eleqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ∈ 𝐶 )
283 22 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
284 26 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
285 283 284 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
286 183 266 282 285 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝐸 ‘ ( 𝐾 − 1 ) ) ‘ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
287 eqcom ⊢ ( ( 𝐾 − 1 ) = ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) ↔ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) )
288 fz1ssfz0 ⊢ ( 1 ... ( ♯ ‘ 𝐼 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐼 ) )
289 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝐼 ) ) ⊆ ℕ0
290 288 289 sstri ⊢ ( 1 ... ( ♯ ‘ 𝐼 ) ) ⊆ ℕ0
291 290 12 sselid ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
292 291 nn0cnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
293 292 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 𝐾 ∈ ℂ )
294 1cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → 1 ∈ ℂ )
295 c0ex ⊢ 0 ∈ V
296 295 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 0 ∈ V )
297 40 34 296 fidmfisupp ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 finSupp 0 )
298 297 296 fsuppres ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ↾ 𝐽 ) finSupp 0 )
299 298 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) finSupp 0 )
300 299 fsuppimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∈ Fin )
301 hashcl ⊢ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∈ Fin → ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) ∈ ℕ0 )
302 300 301 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) ∈ ℕ0 )
303 302 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) ∈ ℂ )
304 293 294 303 subadd2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝐾 − 1 ) = ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) ↔ ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) = 𝐾 ) )
305 287 304 bitr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ↔ ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) = 𝐾 ) )
306 80 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 supp 0 ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) )
307 89 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) )
308 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ¬ ( 𝑓 ‘ 𝑌 ) = 0 )
309 308 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → if ( ( 𝑓 ‘ 𝑌 ) = 0 , ∅ , { 𝑌 } ) = { 𝑌 } )
310 307 309 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) = { 𝑌 } )
311 310 uneq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ ( ( 𝑓 ↾ { 𝑌 } ) supp 0 ) ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ { 𝑌 } ) )
312 306 311 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 𝑓 supp 0 ) = ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ { 𝑌 } ) )
313 312 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) = ( ♯ ‘ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ { 𝑌 } ) ) )
314 suppssdm ⊢ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ⊆ dom ( 𝑓 ↾ 𝐽 )
315 resdmss ⊢ dom ( 𝑓 ↾ 𝐽 ) ⊆ 𝐽
316 314 315 sstri ⊢ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ⊆ 𝐽
317 316 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ⊆ 𝐽 )
318 10 eqimssi ⊢ 𝐽 ⊆ ( 𝐼 ∖ { 𝑌 } )
319 ssdifsn ⊢ ( 𝐽 ⊆ ( 𝐼 ∖ { 𝑌 } ) ↔ ( 𝐽 ⊆ 𝐼 ∧ ¬ 𝑌 ∈ 𝐽 ) )
320 318 319 mpbi ⊢ ( 𝐽 ⊆ 𝐼 ∧ ¬ 𝑌 ∈ 𝐽 )
321 320 simpri ⊢ ¬ 𝑌 ∈ 𝐽
322 321 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ¬ 𝑌 ∈ 𝐽 )
323 317 322 ssneldd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ¬ 𝑌 ∈ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) )
324 hashunsng ⊢ ( 𝑌 ∈ 𝐼 → ( ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∈ Fin ∧ ¬ 𝑌 ∈ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) → ( ♯ ‘ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ { 𝑌 } ) ) = ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) ) )
325 324 imp ⊢ ( ( 𝑌 ∈ 𝐼 ∧ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∈ Fin ∧ ¬ 𝑌 ∈ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) ) → ( ♯ ‘ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ { 𝑌 } ) ) = ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) )
326 237 300 323 325 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ♯ ‘ ( ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ∪ { 𝑌 } ) ) = ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) )
327 313 326 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) = ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) )
328 327 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ↔ ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) + 1 ) = 𝐾 ) )
329 305 328 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ↔ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) )
330 329 anbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) ↔ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) ) )
331 330 ifbid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = ( 𝐾 − 1 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
332 286 331 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( ( 𝐸 ‘ ( 𝐾 − 1 ) ) ‘ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
333 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran 𝑓 ⊆ { 0 , 1 } )
334 164 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 Fn 𝐼 )
335 178 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑌 ∈ 𝐼 )
336 334 335 fnfvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 ‘ 𝑌 ) ∈ ran 𝑓 )
337 333 336 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 ‘ 𝑌 ) ∈ { 0 , 1 } )
338 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ¬ ( 𝑓 ‘ 𝑌 ) = 0 )
339 338 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 ‘ 𝑌 ) ≠ 0 )
340 85 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ‘ 𝑌 ) ∈ ℂ )
341 340 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 ‘ 𝑌 ) ∈ ℂ )
342 1cnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 1 ∈ ℂ )
343 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 )
344 163 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) Fn 𝐼 )
345 130 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝐼 ∈ Fin )
346 334 344 345 335 238 syl22anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = ( ( 𝑓 ‘ 𝑌 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ) )
347 246 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) = 1 )
348 347 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝑓 ‘ 𝑌 ) − ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) ) = ( ( 𝑓 ‘ 𝑌 ) − 1 ) )
349 346 348 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = ( ( 𝑓 ‘ 𝑌 ) − 1 ) )
350 349 eqeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ↔ ( ( 𝑓 ‘ 𝑌 ) − 1 ) = 0 ) )
351 343 350 mtbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ¬ ( ( 𝑓 ‘ 𝑌 ) − 1 ) = 0 )
352 subeq0 ⊢ ( ( ( 𝑓 ‘ 𝑌 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑓 ‘ 𝑌 ) − 1 ) = 0 ↔ ( 𝑓 ‘ 𝑌 ) = 1 ) )
353 352 notbid ⊢ ( ( ( 𝑓 ‘ 𝑌 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ¬ ( ( 𝑓 ‘ 𝑌 ) − 1 ) = 0 ↔ ¬ ( 𝑓 ‘ 𝑌 ) = 1 ) )
354 353 biimpa ⊢ ( ( ( ( 𝑓 ‘ 𝑌 ) ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ¬ ( ( 𝑓 ‘ 𝑌 ) − 1 ) = 0 ) → ¬ ( 𝑓 ‘ 𝑌 ) = 1 )
355 341 342 351 354 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ¬ ( 𝑓 ‘ 𝑌 ) = 1 )
356 355 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 ‘ 𝑌 ) ≠ 1 )
357 339 356 nelprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ¬ ( 𝑓 ‘ 𝑌 ) ∈ { 0 , 1 } )
358 337 357 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ¬ ran 𝑓 ⊆ { 0 , 1 } )
359 358 intnanrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) )
360 359 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
361 360 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) ∧ ¬ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 ) → ( 0g ‘ 𝑅 ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
362 332 361 ifeqda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → if ( ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ‘ 𝑌 ) = 0 , ( ( 𝐸 ‘ ( 𝐾 − 1 ) ) ‘ ( ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
363 176 180 362 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
364 174 363 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
365 100 364 ifeqda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) , ( ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
366 14 365 eqtrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ( +g ‘ 𝑅 ) if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
367 366 mpteq2dva ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐷 ↦ ( if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ( +g ‘ 𝑅 ) if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
368 1 7 8 mplringd ⊢ ( 𝜑 → 𝑊 ∈ Ring )
369 1 2 102 7 8 9 mvrcl ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
370 102 4 368 369 118 ringcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) ∈ ( Base ‘ 𝑊 ) )
371 6 fveq1i ⊢ ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) = ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ 𝐾 ) )
372 11 fveq1i ⊢ ( 𝐸 ‘ 𝐾 ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 )
373 13 111 8 291 105 esplympl ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
374 372 373 eqeltrid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
375 107 374 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑊 ) )
376 371 375 eqeltrid ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑊 ) )
377 1 102 16 3 370 376 mpladd ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) + ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ) = ( ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ) )
378 2 fveq1i ⊢ ( 𝑉 ‘ 𝑌 ) = ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 )
379 eqid ⊢ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } )
380 1 378 102 4 17 5 379 7 9 8 118 mplmulmvr ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) )
381 6 a1i ⊢ ( 𝜑 → 𝐺 = ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) )
382 13 111 8 291 17 20 esplyfval3 ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
383 372 382 eqtrid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐾 ) = ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
384 381 383 fveq12d ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) = ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
385 382 373 eqeltrrd ⊢ ( 𝜑 → ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
386 5 17 7 8 9 10 105 385 extvfv ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑓 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) ) )
387 rneq ⊢ ( 𝑔 = ( 𝑓 ↾ 𝐽 ) → ran 𝑔 = ran ( 𝑓 ↾ 𝐽 ) )
388 387 sseq1d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝐽 ) → ( ran 𝑔 ⊆ { 0 , 1 } ↔ ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ) )
389 oveq1 ⊢ ( 𝑔 = ( 𝑓 ↾ 𝐽 ) → ( 𝑔 supp 0 ) = ( ( 𝑓 ↾ 𝐽 ) supp 0 ) )
390 389 fveqeq2d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝐽 ) → ( ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ↔ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) )
391 388 390 anbi12d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝐽 ) → ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) ↔ ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) ) )
392 391 ifbid ⊢ ( 𝑔 = ( 𝑓 ↾ 𝐽 ) → if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
393 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
394 breq1 ⊢ ( ℎ = ( 𝑓 ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( 𝑓 ↾ 𝐽 ) finSupp 0 ) )
395 35 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ℕ0 ∈ V )
396 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝐽 ∈ Fin )
397 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
398 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → 𝐽 ⊆ 𝐼 )
399 397 398 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
400 395 396 399 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
401 298 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) finSupp 0 )
402 394 400 401 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
403 402 13 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 𝑓 ↾ 𝐽 ) ∈ 𝐶 )
404 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 1r ‘ 𝑅 ) ∈ V )
405 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( 0g ‘ 𝑅 ) ∈ V )
406 404 405 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
407 392 393 403 406 fvmptd4 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑓 ‘ 𝑌 ) = 0 ) → ( ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑓 ↾ 𝐽 ) ) = if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
408 407 ifeq1da ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑓 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) = if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) )
409 408 mpteq2dva ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( ( 𝑔 ∈ 𝐶 ↦ if ( ( ran 𝑔 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑔 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑓 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) )
410 384 386 409 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) )
411 380 410 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ) = ( ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) )
412 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
413 5 412 rabex2 ⊢ 𝐷 ∈ V
414 413 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
415 nfv ⊢ Ⅎ 𝑓 𝜑
416 fvexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ∈ V )
417 26 416 ifexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ∈ V )
418 eqid ⊢ ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) )
419 415 417 418 fnmptd ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) Fn 𝐷 )
420 27 26 ifcld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
421 eqid ⊢ ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) )
422 415 420 421 fnmptd ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) Fn 𝐷 )
423 ofmpteq ⊢ ( ( 𝐷 ∈ V ∧ ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) Fn 𝐷 ∧ ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) Fn 𝐷 ) → ( ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ 𝐷 ↦ ( if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ( +g ‘ 𝑅 ) if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) )
424 414 419 422 423 syl3anc ⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑓 ∈ 𝐷 ↦ if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ 𝐷 ↦ ( if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ( +g ‘ 𝑅 ) if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) )
425 377 411 424 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) + ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ) = ( 𝑓 ∈ 𝐷 ↦ ( if ( ( 𝑓 ‘ 𝑌 ) = 0 , ( 0g ‘ 𝑅 ) , ( ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ‘ ( 𝑓 ∘f − ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ) ) ) ( +g ‘ 𝑅 ) if ( ( 𝑓 ‘ 𝑌 ) = 0 , if ( ( ran ( 𝑓 ↾ 𝐽 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑓 ↾ 𝐽 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) ) )
426 5 7 8 291 17 20 esplyfval3 ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
427 367 425 426 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ( 𝑉 ‘ 𝑌 ) · ( 𝐺 ‘ ( 𝐸 ‘ ( 𝐾 − 1 ) ) ) ) + ( 𝐺 ‘ ( 𝐸 ‘ 𝐾 ) ) ) )