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