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