Metamath Proof Explorer

Theorem reprsuc

Description: Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
reprsuc.f ⊢ 𝐹 = ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
Assertion reprsuc ( 𝜑 → ( 𝐴 ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) = ∪ 𝑏 ∈ 𝐴 ran 𝐹 )

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 reprsuc.f ⊢ 𝐹 = ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
5 1nn0 ⊢ 1 ∈ ℕ0
6 5 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
7 3 6 nn0addcld ⊢ ( 𝜑 → ( 𝑆 + 1 ) ∈ ℕ0 )
8 1 2 7 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
9 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) )
10 elmapi ⊢ ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) → 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
11 9 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
12 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑆 ∈ ℕ0 )
13 fzonn0p1 ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
14 12 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
15 11 14 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ‘ 𝑆 ) ∈ 𝐴 )
16 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑏 = ( 𝑒 ‘ 𝑆 ) ) → 𝑏 = ( 𝑒 ‘ 𝑆 ) )
17 16 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑏 = ( 𝑒 ‘ 𝑆 ) ) → ( 𝑀 − 𝑏 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) )
18 17 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑏 = ( 𝑒 ‘ 𝑆 ) ) → ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) = ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) )
19 opeq2 ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑆 ) → ⟨ 𝑆 , 𝑏 ⟩ = ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ )
20 19 sneqd ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑆 ) → { ⟨ 𝑆 , 𝑏 ⟩ } = { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } )
21 20 uneq2d ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑆 ) → ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) = ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
22 21 eqeq2d ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑆 ) → ( 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ↔ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) ) )
23 22 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑏 = ( 𝑒 ‘ 𝑆 ) ) → ( 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ↔ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) ) )
24 18 23 rexeqbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑏 = ( 𝑒 ‘ 𝑆 ) ) → ( ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ↔ ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) ) )
25 10 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
26 3 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → 𝑆 ∈ ℕ0 )
27 fzossfzop1 ⊢ ( 𝑆 ∈ ℕ0 → ( 0 ..^ 𝑆 ) ⊆ ( 0 ..^ ( 𝑆 + 1 ) ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( 0 ..^ 𝑆 ) ⊆ ( 0 ..^ ( 𝑆 + 1 ) ) )
29 25 28 fssresd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
31 nnex ⊢ ℕ ∈ V
32 31 a1i ⊢ ( 𝜑 → ℕ ∈ V )
33 32 1 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
34 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
35 34 elexi ⊢ ( 0 ..^ 𝑆 ) ∈ V
36 elmapg ⊢ ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
37 33 35 36 sylancl ⊢ ( 𝜑 → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
39 30 38 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
40 34 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
41 nnsscn ⊢ ℕ ⊆ ℂ
42 41 a1i ⊢ ( 𝜑 → ℕ ⊆ ℂ )
43 1 42 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℂ )
45 29 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) ∈ 𝐴 )
46 44 45 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) ∈ ℂ )
47 40 46 fsumcl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) ∈ ℂ )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) ∈ ℂ )
49 43 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → 𝐴 ⊆ ℂ )
50 26 13 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
51 25 50 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( 𝑒 ‘ 𝑆 ) ∈ 𝐴 )
52 49 51 sseldd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( 𝑒 ‘ 𝑆 ) ∈ ℂ )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ‘ 𝑆 ) ∈ ℂ )
54 48 53 pncand ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) − ( 𝑒 ‘ 𝑆 ) ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) )
55 nfv ⊢ Ⅎ 𝑎 ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) )
56 nfcv ⊢ Ⅎ 𝑎 ( 𝑒 ‘ 𝑆 )
57 fzonel ⊢ ¬ 𝑆 ∈ ( 0 ..^ 𝑆 )
58 57 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ¬ 𝑆 ∈ ( 0 ..^ 𝑆 ) )
59 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
60 28 sselda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
61 59 60 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) ∈ 𝐴 )
62 44 61 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) ∈ ℂ )
63 fveq2 ⊢ ( 𝑎 = 𝑆 → ( 𝑒 ‘ 𝑎 ) = ( 𝑒 ‘ 𝑆 ) )
64 55 56 40 26 58 62 63 52 fsumsplitsn ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → Σ 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ( 𝑒 ‘ 𝑎 ) = ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) )
65 fzosplitsn ⊢ ( 𝑆 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
66 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
67 65 66 eleq2s ⊢ ( 𝑆 ∈ ℕ0 → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
68 26 67 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
69 68 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = Σ 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ( 𝑒 ‘ 𝑎 ) )
70 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
71 70 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) = ( 𝑒 ‘ 𝑎 ) )
72 71 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) )
73 72 oveq1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) = ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) )
74 64 69 73 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) )
76 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 )
77 75 76 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) = 𝑀 )
78 77 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) − ( 𝑒 ‘ 𝑆 ) ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) )
79 54 78 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) )
80 39 79 jca ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) )
81 fveq1 ⊢ ( 𝑑 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑎 ) = ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) )
82 81 sumeq2sdv ⊢ ( 𝑑 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) )
83 82 eqeq1d ⊢ ( 𝑑 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) )
84 83 elrab ⊢ ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) } ↔ ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) )
85 80 84 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) } )
86 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝐴 ⊆ ℕ )
87 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑀 ∈ ℤ )
88 nnssz ⊢ ℕ ⊆ ℤ
89 1 88 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
90 89 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝐴 ⊆ ℤ )
91 90 15 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ‘ 𝑆 ) ∈ ℤ )
92 87 91 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ∈ ℤ )
93 86 92 12 reprval ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) = { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) } )
94 85 93 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) )
95 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑐 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ) → 𝑐 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) )
96 95 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑐 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ) → ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) = ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
97 96 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ∧ 𝑐 = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ) → ( 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) ↔ 𝑒 = ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) ) )
98 11 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑒 Fn ( 0 ..^ ( 𝑆 + 1 ) ) )
99 fnsnsplit ⊢ ( ( 𝑒 Fn ( 0 ..^ ( 𝑆 + 1 ) ) ∧ 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → 𝑒 = ( ( 𝑒 ↾ ( ( 0 ..^ ( 𝑆 + 1 ) ) ∖ { 𝑆 } ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
100 98 14 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑒 = ( ( 𝑒 ↾ ( ( 0 ..^ ( 𝑆 + 1 ) ) ∖ { 𝑆 } ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
101 12 66 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑆 ∈ ( ℤ≥ ‘ 0 ) )
102 fzodif2 ⊢ ( 𝑆 ∈ ( ℤ≥ ‘ 0 ) → ( ( 0 ..^ ( 𝑆 + 1 ) ) ∖ { 𝑆 } ) = ( 0 ..^ 𝑆 ) )
103 101 102 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( ( 0 ..^ ( 𝑆 + 1 ) ) ∖ { 𝑆 } ) = ( 0 ..^ 𝑆 ) )
104 103 reseq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( 𝑒 ↾ ( ( 0 ..^ ( 𝑆 + 1 ) ) ∖ { 𝑆 } ) ) = ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) )
105 104 uneq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ( ( 𝑒 ↾ ( ( 0 ..^ ( 𝑆 + 1 ) ) ∖ { 𝑆 } ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) = ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
106 100 105 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → 𝑒 = ( ( 𝑒 ↾ ( 0 ..^ 𝑆 ) ) ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
107 94 97 106 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − ( 𝑒 ‘ 𝑆 ) ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , ( 𝑒 ‘ 𝑆 ) ⟩ } ) )
108 15 24 107 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) → ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
109 108 anasss ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ) → ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
110 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
111 1 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝐴 ⊆ ℕ )
112 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝐴 ⊆ ℕ )
113 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
114 89 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ ℤ )
115 113 114 zsubcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( 𝑀 − 𝑏 ) ∈ ℤ )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑀 − 𝑏 ) ∈ ℤ )
117 3 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑆 ∈ ℕ0 )
118 117 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑆 ∈ ℕ0 )
119 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) )
120 112 116 118 119 reprf ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
121 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑏 ∈ 𝐴 )
122 118 121 fsnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } : { 𝑆 } ⟶ 𝐴 )
123 fzodisjsn ⊢ ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅
124 123 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ )
125 120 122 124 fun2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ⟶ 𝐴 )
126 118 67 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
127 126 feq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 ↔ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ⟶ 𝐴 ) )
128 125 127 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
129 ovex ⊢ ( 0 ..^ ( 𝑆 + 1 ) ) ∈ V
130 elmapg ⊢ ( ( 𝐴 ∈ V ∧ ( 0 ..^ ( 𝑆 + 1 ) ) ∈ V ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ↔ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 ) )
131 33 129 130 sylancl ⊢ ( 𝜑 → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ↔ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 ) )
132 131 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ↔ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 ) )
133 128 132 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) )
134 133 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) )
135 110 134 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) )
136 126 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
137 136 sumeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = Σ 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ( 𝑒 ‘ 𝑎 ) )
138 nfv ⊢ Ⅎ 𝑎 ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
139 34 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
140 118 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑆 ∈ ℕ0 )
141 57 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ¬ 𝑆 ∈ ( 0 ..^ 𝑆 ) )
142 43 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℂ )
143 128 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
144 110 feq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 ↔ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 ) )
145 143 144 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
146 145 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑒 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ 𝐴 )
147 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
148 elun1 ⊢ ( 𝑎 ∈ ( 0 ..^ 𝑆 ) → 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
149 147 148 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
150 126 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
151 149 150 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
152 146 151 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) ∈ 𝐴 )
153 142 152 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) ∈ ℂ )
154 43 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝐴 ⊆ ℂ )
155 140 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
156 145 155 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 ‘ 𝑆 ) ∈ 𝐴 )
157 154 156 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 ‘ 𝑆 ) ∈ ℂ )
158 138 56 139 140 141 153 63 157 fsumsplitsn ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → Σ 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ( 𝑒 ‘ 𝑎 ) = ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) )
159 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
160 159 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) = ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) )
161 120 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑐 Fn ( 0 ..^ 𝑆 ) )
162 161 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑐 Fn ( 0 ..^ 𝑆 ) )
163 122 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } )
164 163 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } )
165 123 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ )
166 fvun1 ⊢ ( ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } ∧ ( ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) = ( 𝑐 ‘ 𝑎 ) )
167 162 164 165 147 166 syl112anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) = ( 𝑐 ‘ 𝑎 ) )
168 160 167 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) = ( 𝑐 ‘ 𝑎 ) )
169 168 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) = ( 𝑐 ‘ 𝑎 ) )
170 169 sumeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) )
171 112 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝐴 ⊆ ℕ )
172 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑀 − 𝑏 ) ∈ ℤ )
173 119 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) )
174 171 172 140 173 reprsum ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = ( 𝑀 − 𝑏 ) )
175 170 174 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) = ( 𝑀 − 𝑏 ) )
176 110 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 ‘ 𝑆 ) = ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) )
177 161 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑐 Fn ( 0 ..^ 𝑆 ) )
178 163 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } )
179 123 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ )
180 snidg ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ { 𝑆 } )
181 140 180 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑆 ∈ { 𝑆 } )
182 fvun2 ⊢ ( ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } ∧ ( ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ ∧ 𝑆 ∈ { 𝑆 } ) ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) = ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) )
183 177 178 179 181 182 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) = ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) )
184 121 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑏 ∈ 𝐴 )
185 fvsng ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑏 ∈ 𝐴 ) → ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) = 𝑏 )
186 140 184 185 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) = 𝑏 )
187 176 183 186 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 ‘ 𝑆 ) = 𝑏 )
188 175 187 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) = ( ( 𝑀 − 𝑏 ) + 𝑏 ) )
189 zsscn ⊢ ℤ ⊆ ℂ
190 113 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑀 ∈ ℤ )
191 189 190 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑀 ∈ ℂ )
192 187 157 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑏 ∈ ℂ )
193 191 192 npcand ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( ( 𝑀 − 𝑏 ) + 𝑏 ) = 𝑀 )
194 188 193 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑒 ‘ 𝑎 ) + ( 𝑒 ‘ 𝑆 ) ) = 𝑀 )
195 137 158 194 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 )
196 135 195 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) )
197 196 r19.29ffa ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) )
198 109 197 impbida ⊢ ( 𝜑 → ( ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ↔ ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
199 vex ⊢ 𝑐 ∈ V
200 snex ⊢ { ⟨ 𝑆 , 𝑏 ⟩ } ∈ V
201 199 200 unex ⊢ ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ V
202 4 201 elrnmpti ⊢ ( 𝑒 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
203 202 rexbii ⊢ ( ∃ 𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 ↔ ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑒 = ( 𝑐 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
204 198 203 bitr4di ⊢ ( 𝜑 → ( ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 ) )
205 fveq1 ⊢ ( 𝑐 = 𝑒 → ( 𝑐 ‘ 𝑎 ) = ( 𝑒 ‘ 𝑎 ) )
206 205 sumeq2sdv ⊢ ( 𝑐 = 𝑒 → Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) )
207 206 eqeq1d ⊢ ( 𝑐 = 𝑒 → ( Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ↔ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) )
208 207 cbvrabv ⊢ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = { 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 }
209 208 rabeq2i ⊢ ( 𝑒 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝑒 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑒 ‘ 𝑎 ) = 𝑀 ) )
210 eliun ⊢ ( 𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ↔ ∃ 𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 )
211 204 209 210 3bitr4g ⊢ ( 𝜑 → ( 𝑒 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ 𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ) )
212 211 eqrdv ⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ ( 𝑆 + 1 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∪ 𝑏 ∈ 𝐴 ran 𝐹 )
213 8 212 eqtrd ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) = ∪ 𝑏 ∈ 𝐴 ran 𝐹 )