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 35244

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 12622	. . . . 5 ⊢ 1 ∈ ℕ₀
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℕ₀)
6	3, 5	nn0addcld 12671	. . 3 ⊢ (𝜑 → (𝑆 + 1) ∈ ℕ₀)
7	1, 2, 6	reprval 35239	. 2 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀})
8		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
9		elmapi 8869	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
10	8, 9	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
11	3	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ ℕ₀)
12		fzonn0p1 13877	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ (0..^(𝑆 + 1)))
13	11, 12	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
14	10, 13	ffvelcdmd 7085	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ 𝐴)
15		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → 𝑏 = (𝑒‘𝑆))
16	15	oveq2d 7436	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑀 − 𝑏) = (𝑀 − (𝑒‘𝑆)))
17	16	oveq2d 7436	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝐴(repr‘𝑆)(𝑀 − 𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
18		opeq2 4834	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑒‘𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒‘𝑆)⟩)
19	18	sneqd 4596	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑒‘𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒‘𝑆)⟩})
20	19	uneq2d 4115	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
21	20	eqeq2d 2772	. . . . . . . . . 10 ⊢ (𝑏 = (𝑒‘𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
22	21	adantl 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
23	17, 22	rexeqbidv 3336	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
24	9	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
25	3	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ₀)
26		fzossfzop1 13878	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ ℕ₀ → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
27	25, 26	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
28	24, 27	fssresd 6749	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
29	28	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30		nnex 12341	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ ∈ V)
32	31, 1	ssexd 5286	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
33		fzofi 14117	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑆) ∈ Fin
34	33	elexi 3473	. . . . . . . . . . . . . . 15 ⊢ (0..^𝑆) ∈ V
35		elmapg 8859	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
36	32, 34, 35	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
37	36	ad2antrr 739	. . . . . . . . . . . . 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 12340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℂ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℕ ⊆ ℂ)
42	1, 41	sstrd 3941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
43	42	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
44	28	ffvelcdmda 7084	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
45	43, 44	sseldd 3932	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
46	39, 45	fsumcl 15899	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
47	46	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
48	42	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
49	25, 12	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
50	24, 49	ffvelcdmd 7085	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ 𝐴)
51	48, 50	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ ℂ)
52	51	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℂ)
53	47, 52	pncand 11670	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
55		nfcv 2923	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎(𝑒‘𝑆)
56		fzonel 13808	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 𝑆 ∈ (0..^𝑆)
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
58	24	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
59	27	sselda 3931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
60	58, 59	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
61	43, 60	sseldd 3932	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
62		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑆 → (𝑒‘𝑎) = (𝑒‘𝑆))
63	54, 55, 39, 25, 57, 61, 62, 51	fsumsplitsn 15910	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
64		fzosplitsn 13911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (ℤ_≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65		nn0uz 13003	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
66	64, 65	eleq2s 2879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ ℕ₀ → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
67	25, 66	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
68	67	sumeq1d 15867	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
69		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
70	69	fvresd 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒‘𝑎))
71	70	sumeq2dv 15869	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎))
72	71	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
73	63, 68, 72	3eqtr4d 2806	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
74	73	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)))
75		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
76	74, 75	eqtr3d 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = 𝑀)
77	76	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = (𝑀 − (𝑒‘𝑆)))
78	53, 77	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))
79	38, 78	jca 521	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑_m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
80		fveq1 6884	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑‘𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
81	80	sumeq2sdv 15870	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
82	81	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))))
83	82	elrab 3645	. . . . . . . . . . 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 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
86	2	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87		nnssz 12715	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℤ
88	1, 87	sstrdi 3943	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
89	88	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
90	89, 14	sseldd 3932	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℤ)
91	86, 90	zsubcld 12808	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑀 − (𝑒‘𝑆)) ∈ ℤ)
92	85, 91, 11	reprval 35239	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))) = {𝑑 ∈ (𝐴 ↑_m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))})
93	84, 92	eleqtrrd 2864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))))
94		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
95	94	uneq1d 4114	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
96	95	eqeq2d 2772	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩})))
97	10	ffnd 6710	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98		fnsnsplit 7189	. . . . . . . . . . 11 ⊢ ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
99	97, 13, 98	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
100	11, 65	eleqtrdi 2871	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (ℤ_≥‘0))
101		fzodif2 33383	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℤ_≥‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102	100, 101	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103	102	reseq2d 5970	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104	103	uneq1d 4114	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
105	99, 104	eqtrd 2796	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
106	93, 96, 105	rspcedvd 3579	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒‘𝑆)⟩}))
107	14, 23, 106	rspcedvd 3579	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108	107	anasss 472	. . . . . 6 ⊢ ((𝜑 ∧ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109		simpr 490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
110	1	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℕ)
111	110	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝐴 ⊆ ℕ)
112	2	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ ℤ)
113	88	sselda 3931	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℤ)
114	112, 113	zsubcld 12808	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝑀 − 𝑏) ∈ ℤ)
115	114	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ)
116	3	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑆 ∈ ℕ₀)
117	116	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ ℕ₀)
118		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
119	111, 115, 117, 118	reprf 35241	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ 𝐴)
121	117, 120	fsnd 6869	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122		fzodisjsn 13832	. . . . . . . . . . . . . 14 ⊢ ((0..^𝑆) ∩ {𝑆}) = ∅
123	122	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124	119, 121, 123	fun2d 6746	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125	117, 66	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126	125	feq2d 6693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127	124, 126	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128		ovex 7453	. . . . . . . . . . . . 13 ⊢ (0..^(𝑆 + 1)) ∈ V
129		elmapg 8859	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
130	32, 128, 129	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131	130	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132	127, 131	mpbird 260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
133	132	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
134	109, 133	eqeltrd 2861	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))))
135	125	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136	135	sumeq1d 15867	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎))
137		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
138	33	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139	117	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ₀)
140	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
141	42	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142	127	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143	109	feq1d 6691	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144	142, 143	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145	144	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147		elun1 4128	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148	146, 147	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149	125	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150	148, 149	eleqtrrd 2864	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151	145, 150	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴)
152	141, 151	sseldd 3932	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ)
153	42	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154	139, 12	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155	144, 154	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ 𝐴)
156	153, 155	sseldd 3932	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) ∈ ℂ)
157	137, 55, 138, 139, 140, 152, 62, 156	fsumsplitsn 15910	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)))
158		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159	158	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160	119	ffnd 6710	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 Fn (0..^𝑆))
161	160	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162	121	ffnd 6710	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163	162	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164	122	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165		fvun1 6976	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
166	161, 163, 164, 146, 165	syl112anc 1401	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐‘𝑎))
167	159, 166	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = (𝑐‘𝑎))
168	167	ralrimiva 3155	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑐‘𝑎))
169	168	sumeq2d 15868	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎))
170	111	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171	115	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀 − 𝑏) ∈ ℤ)
172	118	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)))
173	170, 171, 139, 172	reprsum 35242	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏))
174	169, 173	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑀 − 𝑏))
175	109	fveq1d 6887	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176	160	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177	162	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178	122	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179		snidg 4621	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ {𝑆})
180	139, 179	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181		fvun2 6977	. . . . . . . . . . . . 13 ⊢ ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182	176, 177, 178, 180, 181	syl112anc 1401	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183	120	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ 𝐴)
184		fvsng 7185	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑏 ∈ 𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185	139, 183, 184	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186	175, 182, 185	3eqtrd 2800	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒‘𝑆) = 𝑏)
187	174, 186	oveq12d 7438	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = ((𝑀 − 𝑏) + 𝑏))
188		zsscn 12701	. . . . . . . . . . . 12 ⊢ ℤ ⊆ ℂ
189	112	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190	188, 189	sselid 3929	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191	186, 156	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192	190, 191	npcand 11673	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀 − 𝑏) + 𝑏) = 𝑀)
193	187, 192	eqtrd 2796	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = 𝑀)
194	136, 157, 193	3eqtrd 2800	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)
195	134, 194	jca 521	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
196	195	r19.29ffa 33068	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
197	108, 196	impbida 813	. . . . 5 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198		reprsuc.f	. . . . . . 7 ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199		vex 3455	. . . . . . . 8 ⊢ 𝑐 ∈ V
200		snex 5397	. . . . . . . 8 ⊢ {⟨𝑆, 𝑏⟩} ∈ V
201	199, 200	unex 7761	. . . . . . 7 ⊢ (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202	198, 201	elrnmpti 5944	. . . . . 6 ⊢ (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203	202	rexbii 3110	. . . . 5 ⊢ (∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204	197, 203	bitr4di 292	. . . 4 ⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹))
205		fveq1 6884	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑎) = (𝑒‘𝑎))
206	205	sumeq2sdv 15870	. . . . . . 7 ⊢ (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎))
207	206	eqeq1d 2763	. . . . . 6 ⊢ (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
208	207	cbvrabv 3423	. . . . 5 ⊢ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = {𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀}
209	208	reqabi 3435	. . . 4 ⊢ (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀))
210		eliun 4955	. . . 4 ⊢ (𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹)
211	204, 209, 210	3bitr4g 317	. . 3 ⊢ (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ 𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹))
212	211	eqrdv 2759	. 2 ⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑_m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
213	7, 212	eqtrd 2796	1 ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 {csn 4584 ⟨cop 4590 ∪ ciun 4951 ↦ cmpt 5186 ran crn 5652 ↾ cres 5653 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ↑_m cmap 8847 Fincfn 8973 ℂcc 11198 0cc0 11200 1c1 11201 + caddc 11203 − cmin 11541 ℕcn 12335 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ..^cfzo 13788 Σcsu 15853 reprcrepr 35237

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-map 8849 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-sum 15854 df-repr 35238

This theorem is used by: breprexplema 35259

W3C validator