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 31996

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 11901	. . . . 5 ⊢ 1 ∈ ℕ₀
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℕ₀)
6	3, 5	nn0addcld 11947	. . 3 ⊢ (𝜑 → (𝑆 + 1) ∈ ℕ₀)
7	1, 2, 6	reprval 31991	. 2 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀})
8		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
9		elmapi 8411	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
11	3	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ ℕ₀)
12		fzonn0p1 13109	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ (0..^(𝑆 + 1)))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
14	10, 13	ffvelrnd 6829	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ 𝐴)
15		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → 𝑏 = (𝑒‘𝑆))
16	15	oveq2d 7151	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑀 − 𝑏) = (𝑀 − (𝑒‘𝑆)))
17	16	oveq2d 7151	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝐴(repr‘𝑆)(𝑀 − 𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
18		opeq2 4765	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑒‘𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒‘𝑆)⟩)
19	18	sneqd 4537	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑒‘𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒‘𝑆)⟩})
20	19	uneq2d 4090	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
21	20	eqeq2d 2809	. . . . . . . . . 10 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
22	21	adantl 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
23	17, 22	rexeqbidv 3355	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
24	9	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
25	3	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ₀)
26		fzossfzop1 13110	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ ℕ₀ → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
28	24, 27	fssresd 6519	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
29	28	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30		nnex 11631	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ ∈ V)
32	31, 1	ssexd 5192	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
33		fzofi 13337	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑆) ∈ Fin
34	33	elexi 3460	. . . . . . . . . . . . . . 15 ⊢ (0..^𝑆) ∈ V
35		elmapg 8402	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
36	32, 34, 35	sylancl 589	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
37	36	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
38	29, 37	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)))
39	33	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin)
40		nnsscn 11630	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℂ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℕ ⊆ ℂ)
42	1, 41	sstrd 3925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
43	42	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
44	28	ffvelrnda 6828	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
45	43, 44	sseldd 3916	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
46	39, 45	fsumcl 15082	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
47	46	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
48	42	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
49	25, 12	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
50	24, 49	ffvelrnd 6829	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ 𝐴)
51	48, 50	sseldd 3916	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ ℂ)
52	51	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℂ)
53	47, 52	pncand 10987	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
55		nfcv 2955	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝑒‘𝑆)
56		fzonel 13046	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 𝑆 ∈ (0..^𝑆)
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
58	24	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
59	27	sselda 3915	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
60	58, 59	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
61	43, 60	sseldd 3916	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
62		fveq2 6645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑆 → (𝑒‘𝑎) = (𝑒‘𝑆))
63	54, 55, 39, 25, 57, 61, 62, 51	fsumsplitsn 15092	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
64		fzosplitsn 13140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (ℤ_≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65		nn0uz 12268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
66	64, 65	eleq2s 2908	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ ℕ₀ → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
67	25, 66	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
68	67	sumeq1d 15050	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
69		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
70	69	fvresd 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒‘𝑎))
71	70	sumeq2dv 15052	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎))
72	71	oveq1d 7150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
73	63, 68, 72	3eqtr4d 2843	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
74	73	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
75		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
76	74, 75	eqtr3d 2835	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = 𝑀)
77	76	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = (𝑀 − (𝑒‘𝑆)))
78	53, 77	eqtr3d 2835	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))
79	38, 78	jca 515	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
80		fveq1 6644	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑‘𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
81	80	sumeq2sdv 15053	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
82	81	eqeq1d 2800	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
83	82	elrab 3628	. . . . . . . . . . 11 ⊢ ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
84	79, 83	sylibr 237	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
85	1	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
86	2	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87		nnssz 11990	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℤ
88	1, 87	sstrdi 3927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
89	88	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
90	89, 14	sseldd 3916	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℤ)
91	86, 90	zsubcld 12080	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑀 − (𝑒‘𝑆)) ∈ ℤ)
92	85, 91, 11	reprval 31991	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))) = {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
93	84, 92	eleqtrrd 2893	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
94		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
95	94	uneq1d 4089	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
96	95	eqeq2d 2809	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
97	10	ffnd 6488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98		fnsnsplit 6923	. . . . . . . . . . 11 ⊢ ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
99	97, 13, 98	syl2anc 587	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
100	11, 65	eleqtrdi 2900	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (ℤ_≥‘0))
101		fzodif2 30541	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℤ_≥‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103	102	reseq2d 5818	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104	103	uneq1d 4089	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
105	99, 104	eqtrd 2833	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
106	93, 96, 105	rspcedvd 3574	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
107	14, 23, 106	rspcedvd 3574	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108	107	anasss 470	. . . . . 6 ⊢ ((𝜑 ∧ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109		simpr 488	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
110	1	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℕ)
111	110	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝐴 ⊆ ℕ)
112	2	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ ℤ)
113	88	sselda 3915	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℤ)
114	112, 113	zsubcld 12080	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝑀 − 𝑏) ∈ ℤ)
115	114	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ)
116	3	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑆 ∈ ℕ₀)
117	116	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ ℕ₀)
118		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
119	111, 115, 117, 118	reprf 31993	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ 𝐴)
121	117, 120	fsnd 6632	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122		fzodisjsn 13070	. . . . . . . . . . . . . 14 ⊢ ((0..^𝑆) ∩ {𝑆}) = ∅
123	122	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124	119, 121, 123	fun2d 6516	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125	117, 66	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126	125	feq2d 6473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127	124, 126	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128		ovex 7168	. . . . . . . . . . . . 13 ⊢ (0..^(𝑆 + 1)) ∈ V
129		elmapg 8402	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
130	32, 128, 129	sylancl 589	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131	130	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132	127, 131	mpbird 260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
133	132	adantr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
134	109, 133	eqeltrd 2890	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
135	125	adantr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136	135	sumeq1d 15050	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
137		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
138	33	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139	117	adantr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ₀)
140	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
141	42	ad4antr 731	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142	127	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143	109	feq1d 6472	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144	142, 143	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145	144	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147		elun1 4103	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148	146, 147	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149	125	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150	148, 149	eleqtrrd 2893	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151	145, 150	ffvelrnd 6829	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
152	141, 151	sseldd 3916	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
153	42	ad3antrrr 729	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154	139, 12	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155	144, 154	ffvelrnd 6829	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ 𝐴)
156	153, 155	sseldd 3916	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ ℂ)
157	137, 55, 138, 139, 140, 152, 62, 156	fsumsplitsn 15092	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
158		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159	158	fveq1d 6647	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160	119	ffnd 6488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 Fn (0..^𝑆))
161	160	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162	121	ffnd 6488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163	162	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164	122	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165		fvun1 6729	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
166	161, 163, 164, 146, 165	syl112anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
167	159, 166	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = (𝑐‘𝑎))
168	167	ralrimiva 3149	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑐‘𝑎))
169	168	sumeq2d 15051	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎))
170	111	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171	115	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀 − 𝑏) ∈ ℤ)
172	118	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
173	170, 171, 139, 172	reprsum 31994	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏))
174	169, 173	eqtrd 2833	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑀 − 𝑏))
175	109	fveq1d 6647	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176	160	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177	162	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178	122	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179		snidg 4559	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ {𝑆})
180	139, 179	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181		fvun2 6730	. . . . . . . . . . . . 13 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182	176, 177, 178, 180, 181	syl112anc 1371	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183	120	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ 𝐴)
184		fvsng 6919	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑏 ∈ 𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185	139, 183, 184	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186	175, 182, 185	3eqtrd 2837	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = 𝑏)
187	174, 186	oveq12d 7153	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = ((𝑀 − 𝑏) + 𝑏))
188		zsscn 11977	. . . . . . . . . . . 12 ⊢ ℤ ⊆ ℂ
189	112	ad2antrr 725	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190	188, 189	sseldi 3913	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191	186, 156	eqeltrrd 2891	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192	190, 191	npcand 10990	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀 − 𝑏) + 𝑏) = 𝑀)
193	187, 192	eqtrd 2833	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = 𝑀)
194	136, 157, 193	3eqtrd 2837	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
195	134, 194	jca 515	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
196	195	r19.29ffa 30244	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
197	108, 196	impbida 800	. . . . 5 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198		reprsuc.f	. . . . . . 7 ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199		vex 3444	. . . . . . . 8 ⊢ 𝑐 ∈ V
200		snex 5297	. . . . . . . 8 ⊢ {⟨𝑆, 𝑏⟩} ∈ V
201	199, 200	unex 7449	. . . . . . 7 ⊢ (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202	198, 201	elrnmpti 5796	. . . . . 6 ⊢ (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203	202	rexbii 3210	. . . . 5 ⊢ (∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204	197, 203	syl6bbr 292	. . . 4 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹))
205		fveq1 6644	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑎) = (𝑒‘𝑎))
206	205	sumeq2sdv 15053	. . . . . . 7 ⊢ (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎))
207	206	eqeq1d 2800	. . . . . 6 ⊢ (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
208	207	cbvrabv 3439	. . . . 5 ⊢ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = {𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀}
209	208	rabeq2i 3435	. . . 4 ⊢ (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
210		eliun 4885	. . . 4 ⊢ (𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹)
211	204, 209, 210	3bitr4g 317	. . 3 ⊢ (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ 𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹))
212	211	eqrdv 2796	. 2 ⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
213	7, 212	eqtrd 2833	1 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∃wrex 3107 {crab 3110 Vcvv 3441 ∖ cdif 3878 ∪ cun 3879 ∩ cin 3880 ⊆ wss 3881 ∅c0 4243 {csn 4525 ⟨cop 4531 ∪ ciun 4881 ↦ cmpt 5110 ran crn 5520 ↾ cres 5521 Fn wfn 6319 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ↑_m cmap 8389 Fincfn 8492 ℂcc 10524 0cc0 10526 1c1 10527 + caddc 10529 − cmin 10859 ℕcn 11625 ℕ₀cn0 11885 ℤcz 11969 ℤ_≥cuz 12231 ..^cfzo 13028 Σcsu 15034 reprcrepr 31989

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-sup 8890 df-oi 8958 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-n0 11886 df-z 11970 df-uz 12232 df-rp 12378 df-fz 12886 df-fzo 13029 df-seq 13365 df-exp 13426 df-hash 13687 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-clim 14837 df-sum 15035 df-repr 31990

This theorem is referenced by: breprexplema 32011

W3C validator