Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reprsuc Structured version   Visualization version   GIF version

Theorem reprsuc 31791
 Description: Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
Hypotheses
Ref Expression
reprval.a (𝜑𝐴 ⊆ ℕ)
reprval.m (𝜑𝑀 ∈ ℤ)
reprval.s (𝜑𝑆 ∈ ℕ0)
reprsuc.f 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
Assertion
Ref Expression
reprsuc (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
Distinct variable groups:   𝐴,𝑏,𝑐   𝑀,𝑏,𝑐   𝑆,𝑏,𝑐   𝜑,𝑏,𝑐
Allowed substitution hints:   𝐹(𝑏,𝑐)

Proof of Theorem reprsuc
Dummy variables 𝑎 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reprval.a . . 3 (𝜑𝐴 ⊆ ℕ)
2 reprval.m . . 3 (𝜑𝑀 ∈ ℤ)
3 reprval.s . . . 4 (𝜑𝑆 ∈ ℕ0)
4 1nn0 11907 . . . . 5 1 ∈ ℕ0
54a1i 11 . . . 4 (𝜑 → 1 ∈ ℕ0)
63, 5nn0addcld 11953 . . 3 (𝜑 → (𝑆 + 1) ∈ ℕ0)
71, 2, 6reprval 31786 . 2 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀})
8 simplr 765 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 ∈ (𝐴m (0..^(𝑆 + 1))))
9 elmapi 8423 . . . . . . . . . 10 (𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
108, 9syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
113ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ ℕ0)
12 fzonn0p1 13109 . . . . . . . . . 10 (𝑆 ∈ ℕ0𝑆 ∈ (0..^(𝑆 + 1)))
1311, 12syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
1410, 13ffvelrnd 6850 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ 𝐴)
15 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → 𝑏 = (𝑒𝑆))
1615oveq2d 7166 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑀𝑏) = (𝑀 − (𝑒𝑆)))
1716oveq2d 7166 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝐴(repr‘𝑆)(𝑀𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
18 opeq2 4803 . . . . . . . . . . . . 13 (𝑏 = (𝑒𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒𝑆)⟩)
1918sneqd 4576 . . . . . . . . . . . 12 (𝑏 = (𝑒𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒𝑆)⟩})
2019uneq2d 4143 . . . . . . . . . . 11 (𝑏 = (𝑒𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
2120eqeq2d 2837 . . . . . . . . . 10 (𝑏 = (𝑒𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2221adantl 482 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2317, 22rexeqbidv 3408 . . . . . . . 8 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
249adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
253adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ0)
26 fzossfzop1 13110 . . . . . . . . . . . . . . . 16 (𝑆 ∈ ℕ0 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2725, 26syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2824, 27fssresd 6544 . . . . . . . . . . . . . 14 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
2928adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30 nnex 11638 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
3130a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℕ ∈ V)
3231, 1ssexd 5225 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
33 fzofi 13337 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
3433elexi 3519 . . . . . . . . . . . . . . 15 (0..^𝑆) ∈ V
35 elmapg 8414 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3632, 34, 35sylancl 586 . . . . . . . . . . . . . 14 (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3736ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3829, 37mpbird 258 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴m (0..^𝑆)))
3933a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin)
40 nnsscn 11637 . . . . . . . . . . . . . . . . . . . 20 ℕ ⊆ ℂ
4140a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℕ ⊆ ℂ)
421, 41sstrd 3981 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
4342ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
4428ffvelrnda 6849 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
4543, 44sseldd 3972 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4639, 45fsumcl 15085 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4746adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4842adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
4925, 12syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
5024, 49ffvelrnd 6850 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ 𝐴)
5148, 50sseldd 3972 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ ℂ)
5251adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℂ)
5347, 52pncand 10992 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54 nfv 1908 . . . . . . . . . . . . . . . . . 18 𝑎(𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1))))
55 nfcv 2982 . . . . . . . . . . . . . . . . . 18 𝑎(𝑒𝑆)
56 fzonel 13046 . . . . . . . . . . . . . . . . . . 19 ¬ 𝑆 ∈ (0..^𝑆)
5756a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
5824adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
5927sselda 3971 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
6058, 59ffvelrnd 6850 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
6143, 60sseldd 3972 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
62 fveq2 6669 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑆 → (𝑒𝑎) = (𝑒𝑆))
6354, 55, 39, 25, 57, 61, 62, 51fsumsplitsn 15095 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
64 fzosplitsn 13140 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ (ℤ‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65 nn0uz 12274 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
6664, 65eleq2s 2936 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ ℕ0 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6725, 66syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6867sumeq1d 15053 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
69 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
7069fvresd 6689 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒𝑎))
7170sumeq2dv 15055 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎))
7271oveq1d 7165 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
7363, 68, 723eqtr4d 2871 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
7473adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
75 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
7674, 75eqtr3d 2863 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = 𝑀)
7776oveq1d 7165 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = (𝑀 − (𝑒𝑆)))
7853, 77eqtr3d 2863 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆)))
7938, 78jca 512 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
80 fveq1 6668 . . . . . . . . . . . . . 14 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
8180sumeq2sdv 15056 . . . . . . . . . . . . 13 (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
8281eqeq1d 2828 . . . . . . . . . . . 12 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8382elrab 3684 . . . . . . . . . . 11 ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8479, 83sylibr 235 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
851ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
862ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87 nnssz 11996 . . . . . . . . . . . . . . 15 ℕ ⊆ ℤ
881, 87sstrdi 3983 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℤ)
8988ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
9089, 14sseldd 3972 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℤ)
9186, 90zsubcld 12086 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑀 − (𝑒𝑆)) ∈ ℤ)
9285, 91, 11reprval 31786 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))) = {𝑑 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
9384, 92eleqtrrd 2921 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
94 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
9594uneq1d 4142 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9695eqeq2d 2837 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩})))
9710ffnd 6514 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98 fnsnsplit 6944 . . . . . . . . . . 11 ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9997, 13, 98syl2anc 584 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10011, 65syl6eleq 2928 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (ℤ‘0))
101 fzodif2 30447 . . . . . . . . . . . . 13 (𝑆 ∈ (ℤ‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102100, 101syl 17 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103102reseq2d 5852 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104103uneq1d 4142 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10599, 104eqtrd 2861 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10693, 96, 105rspcedvd 3630 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10714, 23, 106rspcedvd 3630 . . . . . . 7 (((𝜑𝑒 ∈ (𝐴m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108107anasss 467 . . . . . 6 ((𝜑 ∧ (𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109 simpr 485 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
1101adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝐴 ⊆ ℕ)
111110adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝐴 ⊆ ℕ)
1122adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑀 ∈ ℤ)
11388sselda 3971 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑏 ∈ ℤ)
114112, 113zsubcld 12086 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → (𝑀𝑏) ∈ ℤ)
115114adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑀𝑏) ∈ ℤ)
1163adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝑆 ∈ ℕ0)
117116adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ ℕ0)
118 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
119111, 115, 117, 118reprf 31788 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120 simplr 765 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑏𝐴)
121117, 120fsnd 6656 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122 fzodisjsn 13070 . . . . . . . . . . . . . 14 ((0..^𝑆) ∩ {𝑆}) = ∅
123122a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124119, 121, 123fun2d 6541 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125117, 66syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126125feq2d 6499 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127124, 126mpbird 258 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128 ovex 7183 . . . . . . . . . . . . 13 (0..^(𝑆 + 1)) ∈ V
129 elmapg 8414 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
13032, 128, 129sylancl 586 . . . . . . . . . . . 12 (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131130ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132127, 131mpbird 258 . . . . . . . . . 10 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴m (0..^(𝑆 + 1))))
133132adantr 481 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴m (0..^(𝑆 + 1))))
134109, 133eqeltrd 2918 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴m (0..^(𝑆 + 1))))
135125adantr 481 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136135sumeq1d 15053 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
137 nfv 1908 . . . . . . . . . 10 𝑎(((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
13833a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139117adantr 481 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ0)
14056a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
14142ad4antr 728 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142127adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143109feq1d 6498 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144142, 143mpbird 258 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145144adantr 481 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146 simpr 485 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147 elun1 4156 . . . . . . . . . . . . . 14 (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148146, 147syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149125ad2antrr 722 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150148, 149eleqtrrd 2921 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151145, 150ffvelrnd 6850 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
152141, 151sseldd 3972 . . . . . . . . . 10 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
15342ad3antrrr 726 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154139, 12syl 17 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155144, 154ffvelrnd 6850 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ 𝐴)
156153, 155sseldd 3972 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ ℂ)
157137, 55, 138, 139, 140, 152, 62, 156fsumsplitsn 15095 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
158 simplr 765 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159158fveq1d 6671 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160119ffnd 6514 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 Fn (0..^𝑆))
161160ad2antrr 722 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162121ffnd 6514 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163162ad2antrr 722 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164122a1i 11 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165 fvun1 6753 . . . . . . . . . . . . . . . 16 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
166161, 163, 164, 146, 165syl112anc 1368 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
167159, 166eqtrd 2861 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = (𝑐𝑎))
168167ralrimiva 3187 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑐𝑎))
169168sumeq2d 15054 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎))
170111adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171115adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀𝑏) ∈ ℤ)
172118adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
173170, 171, 139, 172reprsum 31789 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = (𝑀𝑏))
174169, 173eqtrd 2861 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑀𝑏))
175109fveq1d 6671 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176160adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177162adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178122a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179 snidg 4596 . . . . . . . . . . . . . 14 (𝑆 ∈ ℕ0𝑆 ∈ {𝑆})
180139, 179syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181 fvun2 6754 . . . . . . . . . . . . 13 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182176, 177, 178, 180, 181syl112anc 1368 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183120adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏𝐴)
184 fvsng 6940 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ0𝑏𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185139, 183, 184syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186175, 182, 1853eqtrd 2865 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = 𝑏)
187174, 186oveq12d 7168 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = ((𝑀𝑏) + 𝑏))
188 zsscn 11983 . . . . . . . . . . . 12 ℤ ⊆ ℂ
189112ad2antrr 722 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190188, 189sseldi 3969 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191186, 156eqeltrrd 2919 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192190, 191npcand 10995 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀𝑏) + 𝑏) = 𝑀)
193187, 192eqtrd 2861 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = 𝑀)
194136, 157, 1933eqtrd 2865 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
195134, 194jca 512 . . . . . . 7 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
196195r19.29ffa 30170 . . . . . 6 ((𝜑 ∧ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
197108, 196impbida 797 . . . . 5 (𝜑 → ((𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198 reprsuc.f . . . . . . 7 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199 vex 3503 . . . . . . . 8 𝑐 ∈ V
200 snex 5328 . . . . . . . 8 {⟨𝑆, 𝑏⟩} ∈ V
201199, 200unex 7462 . . . . . . 7 (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202198, 201elrnmpti 5831 . . . . . 6 (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203202rexbii 3252 . . . . 5 (∃𝑏𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204197, 203syl6bbr 290 . . . 4 (𝜑 → ((𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹))
205 fveq1 6668 . . . . . . . 8 (𝑐 = 𝑒 → (𝑐𝑎) = (𝑒𝑎))
206205sumeq2sdv 15056 . . . . . . 7 (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎))
207206eqeq1d 2828 . . . . . 6 (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
208207cbvrabv 3497 . . . . 5 {𝑐 ∈ (𝐴m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = {𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀}
209208rabeq2i 3493 . . . 4 (𝑒 ∈ {𝑐 ∈ (𝐴m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
210 eliun 4921 . . . 4 (𝑒 𝑏𝐴 ran 𝐹 ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹)
211204, 209, 2103bitr4g 315 . . 3 (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ 𝑒 𝑏𝐴 ran 𝐹))
212211eqrdv 2824 . 2 (𝜑 → {𝑐 ∈ (𝐴m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = 𝑏𝐴 ran 𝐹)
2137, 212eqtrd 2861 1 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530   ∈ wcel 2107  ∃wrex 3144  {crab 3147  Vcvv 3500   ∖ cdif 3937   ∪ cun 3938   ∩ cin 3939   ⊆ wss 3940  ∅c0 4295  {csn 4564  ⟨cop 4570  ∪ ciun 4917   ↦ cmpt 5143  ran crn 5555   ↾ cres 5556   Fn wfn 6349  ⟶wf 6350  ‘cfv 6354  (class class class)co 7150   ↑m cmap 8401  Fincfn 8503  ℂcc 10529  0cc0 10531  1c1 10532   + caddc 10534   − cmin 10864  ℕcn 11632  ℕ0cn0 11891  ℤcz 11975  ℤ≥cuz 12237  ..^cfzo 13028  Σcsu 15037  reprcrepr 31784 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12385  df-fz 12888  df-fzo 13029  df-seq 13365  df-exp 13425  df-hash 13686  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038  df-repr 31785 This theorem is referenced by:  breprexplema  31806
 Copyright terms: Public domain W3C validator