reprsuc - Mathbox for Thierry Arnoux

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

Theorem reprsuc 30693

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

**Hypotheses**
Ref	Expression
reprval.a	⊢ (𝜑 → 𝐴 ⊆ ℕ)
reprval.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
reprval.s	⊢ (𝜑 → 𝑆 ∈ ℕ₀)
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.

Step	Hyp	Ref	Expression
1		reprval.a	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℕ)
2		reprval.m	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		reprval.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ℕ₀)
4		1nn0 11308	. . . . 5 ⊢ 1 ∈ ℕ₀
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℕ₀)
6	3, 5	nn0addcld 11355	. . 3 ⊢ (𝜑 → (𝑆 + 1) ∈ ℕ₀)
7	1, 2, 6	reprval 30688	. 2 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀})
8		simplr 792	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))))
9		elmapi 7879	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
11	3	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ ℕ₀)
12		fzonn0p1 12544	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ (0..^(𝑆 + 1)))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
14	10, 13	ffvelrnd 6360	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ 𝐴)
15		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → 𝑏 = (𝑒‘𝑆))
16	15	oveq2d 6666	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑀 − 𝑏) = (𝑀 − (𝑒‘𝑆)))
17	16	oveq2d 6666	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝐴(repr‘𝑆)(𝑀 − 𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
18		opeq2 4403	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑒‘𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒‘𝑆)⟩)
19	18	sneqd 4189	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑒‘𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒‘𝑆)⟩})
20	19	uneq2d 3767	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
21	20	eqeq2d 2632	. . . . . . . . . 10 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
22	21	adantl 482	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
23	17, 22	rexeqbidv 3153	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
24	9	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
25	3	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ₀)
26		fzossfzop1 12545	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ ℕ₀ → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
28	24, 27	fssresd 6071	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
29	28	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30		nnex 11026	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ ∈ V)
32	31, 1	ssexd 4805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
33		fzofi 12773	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑆) ∈ Fin
34	33	elexi 3213	. . . . . . . . . . . . . . 15 ⊢ (0..^𝑆) ∈ V
35		elmapg 7870	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
36	32, 34, 35	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
37	36	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
38	29, 37	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_𝑚 (0..^𝑆)))
39	33	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin)
40		nnsscn 11025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℂ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℕ ⊆ ℂ)
42	1, 41	sstrd 3613	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
43	42	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
44	28	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
45	43, 44	sseldd 3604	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
46	39, 45	fsumcl 14464	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
47	46	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
48	42	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
49	25, 12	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
50	24, 49	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ 𝐴)
51	48, 50	sseldd 3604	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ ℂ)
52	51	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℂ)
53	47, 52	pncand 10393	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54		nfv 1843	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))))
55		nfcv 2764	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝑒‘𝑆)
56		fzonel 12483	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 𝑆 ∈ (0..^𝑆)
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
58	24	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
59	27	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
60	58, 59	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
61	43, 60	sseldd 3604	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
62		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑆 → (𝑒‘𝑎) = (𝑒‘𝑆))
63	54, 55, 39, 25, 57, 61, 62, 51	fsumsplitsn 14474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
64		fzosplitsn 12576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (ℤ_≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65		nn0uz 11722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
66	64, 65	eleq2s 2719	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ ℕ₀ → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
67	25, 66	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
68	67	sumeq1d 14431	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
69		simpr 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
70	69	fvresd 6208	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒‘𝑎))
71	70	sumeq2dv 14433	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎))
72	71	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
73	63, 68, 72	3eqtr4d 2666	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
74	73	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
75		simpr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
76	74, 75	eqtr3d 2658	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = 𝑀)
77	76	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = (𝑀 − (𝑒‘𝑆)))
78	53, 77	eqtr3d 2658	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))
79	38, 78	jca 554	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
80		fveq1 6190	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑‘𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
81	80	sumeq2sdv 14435	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
82	81	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
83	82	elrab 3363	. . . . . . . . . . 11 ⊢ ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
84	79, 83	sylibr 224	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
85	1	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
86	2	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87		nnssz 11397	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℤ
88	1, 87	syl6ss 3615	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
89	88	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
90	89, 14	sseldd 3604	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℤ)
91	86, 90	zsubcld 11487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑀 − (𝑒‘𝑆)) ∈ ℤ)
92	85, 91, 11	reprval 30688	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))) = {𝑑 ∈ (𝐴 ↑_𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
93	84, 92	eleqtrrd 2704	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
94		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
95	94	uneq1d 3766	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
96	95	eqeq2d 2632	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
97	10	ffnd 6046	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98		fnsnsplit 6450	. . . . . . . . . . 11 ⊢ ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
99	97, 13, 98	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
100	11, 65	syl6eleq 2711	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (ℤ_≥‘0))
101		fzodif2 29552	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℤ_≥‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103	102	reseq2d 5396	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104	103	uneq1d 3766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
105	99, 104	eqtrd 2656	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
106	93, 96, 105	rspcedvd 3317	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
107	14, 23, 106	rspcedvd 3317	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108	107	anasss 679	. . . . . 6 ⊢ ((𝜑 ∧ (𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109		simpr 477	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
110	1	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℕ)
111	110	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝐴 ⊆ ℕ)
112	2	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ ℤ)
113	88	sselda 3603	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℤ)
114	112, 113	zsubcld 11487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝑀 − 𝑏) ∈ ℤ)
115	114	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ)
116	3	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑆 ∈ ℕ₀)
117	116	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ ℕ₀)
118		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
119	111, 115, 117, 118	reprf 30690	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120		simplr 792	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ 𝐴)
121	117, 120	fsnd 6179	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122		fzodisjsn 12505	. . . . . . . . . . . . . 14 ⊢ ((0..^𝑆) ∩ {𝑆}) = ∅
123	122	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124	119, 121, 123	fun2d 6068	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125	117, 66	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126	125	feq2d 6031	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127	124, 126	mpbird 247	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128		ovex 6678	. . . . . . . . . . . . 13 ⊢ (0..^(𝑆 + 1)) ∈ V
129		elmapg 7870	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
130	32, 128, 129	sylancl 694	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131	130	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132	127, 131	mpbird 247	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))))
133	132	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))))
134	109, 133	eqeltrd 2701	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))))
135	125	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136	135	sumeq1d 14431	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
137		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
138	33	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139	117	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ₀)
140	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
141	42	ad4antr 768	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142	127	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143	109	feq1d 6030	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144	142, 143	mpbird 247	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145	144	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147		elun1 3780	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148	146, 147	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149	125	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150	148, 149	eleqtrrd 2704	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151	145, 150	ffvelrnd 6360	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
152	141, 151	sseldd 3604	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
153	42	ad3antrrr 766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154	139, 12	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155	144, 154	ffvelrnd 6360	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ 𝐴)
156	153, 155	sseldd 3604	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ ℂ)
157	137, 55, 138, 139, 140, 152, 62, 156	fsumsplitsn 14474	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
158		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159	158	fveq1d 6193	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160	119	ffnd 6046	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 Fn (0..^𝑆))
161	160	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162	121	ffnd 6046	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163	162	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164	122	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165		fvun1 6269	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
166	161, 163, 164, 146, 165	syl112anc 1330	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
167	159, 166	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = (𝑐‘𝑎))
168	167	ralrimiva 2966	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑐‘𝑎))
169	168	sumeq2d 14432	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎))
170	111	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171	115	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀 − 𝑏) ∈ ℤ)
172	118	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
173	170, 171, 139, 172	reprsum 30691	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏))
174	169, 173	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑀 − 𝑏))
175	109	fveq1d 6193	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176	160	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177	162	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178	122	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179		snidg 4206	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ {𝑆})
180	139, 179	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181		fvun2 6270	. . . . . . . . . . . . 13 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182	176, 177, 178, 180, 181	syl112anc 1330	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183	120	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ 𝐴)
184		fvsng 6447	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑏 ∈ 𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185	139, 183, 184	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186	175, 182, 185	3eqtrd 2660	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = 𝑏)
187	174, 186	oveq12d 6668	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = ((𝑀 − 𝑏) + 𝑏))
188		zsscn 11385	. . . . . . . . . . . 12 ⊢ ℤ ⊆ ℂ
189	112	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190	188, 189	sseldi 3601	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191	186, 156	eqeltrrd 2702	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192	190, 191	npcand 10396	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀 − 𝑏) + 𝑏) = 𝑀)
193	187, 192	eqtrd 2656	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = 𝑀)
194	136, 157, 193	3eqtrd 2660	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
195	134, 194	jca 554	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
196	195	r19.29ffa 29320	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
197	108, 196	impbida 877	. . . . 5 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198		reprsuc.f	. . . . . . 7 ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199		vex 3203	. . . . . . . 8 ⊢ 𝑐 ∈ V
200		snex 4908	. . . . . . . 8 ⊢ {⟨𝑆, 𝑏⟩} ∈ V
201	199, 200	unex 6956	. . . . . . 7 ⊢ (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202	198, 201	elrnmpti 5376	. . . . . 6 ⊢ (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203	202	rexbii 3041	. . . . 5 ⊢ (∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204	197, 203	syl6bbr 278	. . . 4 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹))
205		fveq1 6190	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑎) = (𝑒‘𝑎))
206	205	sumeq2sdv 14435	. . . . . . 7 ⊢ (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎))
207	206	eqeq1d 2624	. . . . . 6 ⊢ (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
208	207	cbvrabv 3199	. . . . 5 ⊢ {𝑐 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = {𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀}
209	208	rabeq2i 3197	. . . 4 ⊢ (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
210		eliun 4524	. . . 4 ⊢ (𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹)
211	204, 209, 210	3bitr4g 303	. . 3 ⊢ (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ 𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹))
212	211	eqrdv 2620	. 2 ⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑_𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
213	7, 212	eqtrd 2656	1 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∃wrex 2913 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 ⟨cop 4183 ∪ ciun 4520 ↦ cmpt 4729 ran crn 5115 ↾ cres 5116 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↑_𝑚 cmap 7857 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 − cmin 10266 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ..^cfzo 12465 Σcsu 14416 reprcrepr 30686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-repr 30687

This theorem is referenced by: breprexplema 30708

W3C validator