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 34778

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 12447	. . . . 5 ⊢ 1 ∈ ℕ₀
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℕ₀)
6	3, 5	nn0addcld 12496	. . 3 ⊢ (𝜑 → (𝑆 + 1) ∈ ℕ₀)
7	1, 2, 6	reprval 34773	. 2 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀})
8		simplr 769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
9		elmapi 8790	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
11	3	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ ℕ₀)
12		fzonn0p1 13691	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ (0..^(𝑆 + 1)))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
14	10, 13	ffvelcdmd 7032	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ 𝐴)
15		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → 𝑏 = (𝑒‘𝑆))
16	15	oveq2d 7377	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑀 − 𝑏) = (𝑀 − (𝑒‘𝑆)))
17	16	oveq2d 7377	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝐴(repr‘𝑆)(𝑀 − 𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
18		opeq2 4818	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑒‘𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒‘𝑆)⟩)
19	18	sneqd 4580	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑒‘𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒‘𝑆)⟩})
20	19	uneq2d 4109	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
21	20	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
22	21	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
23	17, 22	rexeqbidv 3313	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
24	9	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
25	3	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ₀)
26		fzossfzop1 13692	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ ℕ₀ → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
28	24, 27	fssresd 6702	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
29	28	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30		nnex 12174	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ ∈ V)
32	31, 1	ssexd 5262	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
33		fzofi 13930	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑆) ∈ Fin
34	33	elexi 3453	. . . . . . . . . . . . . . 15 ⊢ (0..^𝑆) ∈ V
35		elmapg 8780	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
36	32, 34, 35	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
37	36	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
38	29, 37	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)))
39	33	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin)
40		nnsscn 12173	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℂ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℕ ⊆ ℂ)
42	1, 41	sstrd 3933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
43	42	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
44	28	ffvelcdmda 7031	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
45	43, 44	sseldd 3923	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
46	39, 45	fsumcl 15689	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
47	46	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
48	42	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
49	25, 12	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
50	24, 49	ffvelcdmd 7032	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ 𝐴)
51	48, 50	sseldd 3923	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ ℂ)
52	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℂ)
53	47, 52	pncand 11500	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54		nfv 1916	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
55		nfcv 2899	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝑒‘𝑆)
56		fzonel 13622	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 𝑆 ∈ (0..^𝑆)
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
58	24	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
59	27	sselda 3922	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
60	58, 59	ffvelcdmd 7032	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
61	43, 60	sseldd 3923	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
62		fveq2 6835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑆 → (𝑒‘𝑎) = (𝑒‘𝑆))
63	54, 55, 39, 25, 57, 61, 62, 51	fsumsplitsn 15700	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
64		fzosplitsn 13725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (ℤ_≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65		nn0uz 12820	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
66	64, 65	eleq2s 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ ℕ₀ → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
67	25, 66	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
68	67	sumeq1d 15656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
69		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
70	69	fvresd 6855	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒‘𝑎))
71	70	sumeq2dv 15658	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎))
72	71	oveq1d 7376	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
73	63, 68, 72	3eqtr4d 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
74	73	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
75		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
76	74, 75	eqtr3d 2774	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = 𝑀)
77	76	oveq1d 7376	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = (𝑀 − (𝑒‘𝑆)))
78	53, 77	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))
79	38, 78	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
80		fveq1 6834	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑‘𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
81	80	sumeq2sdv 15659	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
82	81	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
83	82	elrab 3635	. . . . . . . . . . 11 ⊢ ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
84	79, 83	sylibr 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
85	1	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
86	2	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87		nnssz 12540	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℤ
88	1, 87	sstrdi 3935	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
89	88	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
90	89, 14	sseldd 3923	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℤ)
91	86, 90	zsubcld 12632	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑀 − (𝑒‘𝑆)) ∈ ℤ)
92	85, 91, 11	reprval 34773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))) = {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
93	84, 92	eleqtrrd 2840	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
94		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
95	94	uneq1d 4108	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
96	95	eqeq2d 2748	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
97	10	ffnd 6664	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98		fnsnsplit 7133	. . . . . . . . . . 11 ⊢ ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
99	97, 13, 98	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
100	11, 65	eleqtrdi 2847	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (ℤ_≥‘0))
101		fzodif2 32882	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℤ_≥‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103	102	reseq2d 5939	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104	103	uneq1d 4108	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
105	99, 104	eqtrd 2772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
106	93, 96, 105	rspcedvd 3567	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
107	14, 23, 106	rspcedvd 3567	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108	107	anasss 466	. . . . . 6 ⊢ ((𝜑 ∧ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
110	1	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℕ)
111	110	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝐴 ⊆ ℕ)
112	2	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ ℤ)
113	88	sselda 3922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℤ)
114	112, 113	zsubcld 12632	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝑀 − 𝑏) ∈ ℤ)
115	114	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ)
116	3	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑆 ∈ ℕ₀)
117	116	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ ℕ₀)
118		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
119	111, 115, 117, 118	reprf 34775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ 𝐴)
121	117, 120	fsnd 6819	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122		fzodisjsn 13646	. . . . . . . . . . . . . 14 ⊢ ((0..^𝑆) ∩ {𝑆}) = ∅
123	122	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124	119, 121, 123	fun2d 6699	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125	117, 66	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126	125	feq2d 6647	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127	124, 126	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128		ovex 7394	. . . . . . . . . . . . 13 ⊢ (0..^(𝑆 + 1)) ∈ V
129		elmapg 8780	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
130	32, 128, 129	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131	130	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132	127, 131	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
133	132	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
134	109, 133	eqeltrd 2837	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
135	125	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136	135	sumeq1d 15656	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
137		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
138	33	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139	117	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ₀)
140	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
141	42	ad4antr 733	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142	127	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143	109	feq1d 6645	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144	142, 143	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145	144	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147		elun1 4123	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148	146, 147	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149	125	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150	148, 149	eleqtrrd 2840	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151	145, 150	ffvelcdmd 7032	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
152	141, 151	sseldd 3923	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
153	42	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154	139, 12	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155	144, 154	ffvelcdmd 7032	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ 𝐴)
156	153, 155	sseldd 3923	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ ℂ)
157	137, 55, 138, 139, 140, 152, 62, 156	fsumsplitsn 15700	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
158		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159	158	fveq1d 6837	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160	119	ffnd 6664	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 Fn (0..^𝑆))
161	160	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162	121	ffnd 6664	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163	162	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164	122	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165		fvun1 6926	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
166	161, 163, 164, 146, 165	syl112anc 1377	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
167	159, 166	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = (𝑐‘𝑎))
168	167	ralrimiva 3130	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑐‘𝑎))
169	168	sumeq2d 15657	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎))
170	111	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171	115	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀 − 𝑏) ∈ ℤ)
172	118	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
173	170, 171, 139, 172	reprsum 34776	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏))
174	169, 173	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑀 − 𝑏))
175	109	fveq1d 6837	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176	160	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177	162	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178	122	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179		snidg 4605	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ {𝑆})
180	139, 179	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181		fvun2 6927	. . . . . . . . . . . . 13 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182	176, 177, 178, 180, 181	syl112anc 1377	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183	120	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ 𝐴)
184		fvsng 7129	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑏 ∈ 𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185	139, 183, 184	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186	175, 182, 185	3eqtrd 2776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = 𝑏)
187	174, 186	oveq12d 7379	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = ((𝑀 − 𝑏) + 𝑏))
188		zsscn 12526	. . . . . . . . . . . 12 ⊢ ℤ ⊆ ℂ
189	112	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190	188, 189	sselid 3920	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191	186, 156	eqeltrrd 2838	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192	190, 191	npcand 11503	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀 − 𝑏) + 𝑏) = 𝑀)
193	187, 192	eqtrd 2772	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = 𝑀)
194	136, 157, 193	3eqtrd 2776	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
195	134, 194	jca 511	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
196	195	r19.29ffa 32558	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
197	108, 196	impbida 801	. . . . 5 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198		reprsuc.f	. . . . . . 7 ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199		vex 3434	. . . . . . . 8 ⊢ 𝑐 ∈ V
200		snex 5377	. . . . . . . 8 ⊢ {⟨𝑆, 𝑏⟩} ∈ V
201	199, 200	unex 7692	. . . . . . 7 ⊢ (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202	198, 201	elrnmpti 5912	. . . . . 6 ⊢ (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203	202	rexbii 3085	. . . . 5 ⊢ (∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204	197, 203	bitr4di 289	. . . 4 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹))
205		fveq1 6834	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑎) = (𝑒‘𝑎))
206	205	sumeq2sdv 15659	. . . . . . 7 ⊢ (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎))
207	206	eqeq1d 2739	. . . . . 6 ⊢ (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
208	207	cbvrabv 3400	. . . . 5 ⊢ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = {𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀}
209	208	reqabi 3413	. . . 4 ⊢ (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
210		eliun 4938	. . . 4 ⊢ (𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹)
211	204, 209, 210	3bitr4g 314	. . 3 ⊢ (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ 𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹))
212	211	eqrdv 2735	. 2 ⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
213	7, 212	eqtrd 2772	1 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 {crab 3390 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 {csn 4568 ⟨cop 4574 ∪ ciun 4934 ↦ cmpt 5167 ran crn 5626 ↾ cres 5627 Fn wfn 6488 ⟶wf 6489 ‘cfv 6493 (class class class)co 7361 ↑_m cmap 8767 Fincfn 8887 ℂcc 11030 0cc0 11032 1c1 11033 + caddc 11035 − cmin 11371 ℕcn 12168 ℕ₀cn0 12431 ℤcz 12518 ℤ_≥cuz 12782 ..^cfzo 13602 Σcsu 15642 reprcrepr 34771

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1st 7936 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-oi 9419 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-n0 12432 df-z 12519 df-uz 12783 df-rp 12937 df-fz 13456 df-fzo 13603 df-seq 13958 df-exp 14018 df-hash 14287 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-clim 15444 df-sum 15643 df-repr 34772

This theorem is referenced by: breprexplema 34793

W3C validator