Theorem ttgcontlem1 27833

Description: Lemma for % ttgcont . (Contributed by Thierry Arnoux, 24-May-2019.)

Hypotheses

Ref	Expression
ttgval.n	⊢ 𝐺 = (toTG‘𝐻)
ttgitvval.i	⊢ 𝐼 = (Itv‘𝐺)
ttgitvval.b	⊢ 𝑃 = (Base‘𝐻)
ttgitvval.m	⊢ − = (-g‘𝐻)
ttgitvval.s	⊢ · = ( ·𝑠 ‘𝐻)
ttgelitv.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
ttgelitv.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
ttgbtwnid.r	⊢ 𝑅 = (Base‘(Scalar‘𝐻))
ttgbtwnid.2	⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
ttgitvval.p	⊢ + = (+g‘𝐻)
ttgcontlem1.h	⊢ (𝜑 → 𝐻 ∈ ℂVec)
ttgcontlem1.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
ttgcontlem1.n	⊢ (𝜑 → 𝑁 ∈ 𝑃)
ttgcontlem1.o	⊢ (𝜑 → 𝑀 ≠ 0)
ttgcontlem1.p	⊢ (𝜑 → 𝐾 ≠ 0)
ttgcontlem1.q	⊢ (𝜑 → 𝐾 ≠ 1)
ttgcontlem1.r	⊢ (𝜑 → 𝐿 ≠ 𝑀)
ttgcontlem1.s	⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
ttgcontlem1.l	⊢ (𝜑 → 𝐿 ∈ (0[,]1))
ttgcontlem1.k	⊢ (𝜑 → 𝐾 ∈ (0[,]1))
ttgcontlem1.m	⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
ttgcontlem1.y	⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
ttgcontlem1.x	⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
ttgcontlem1.b	⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))

Assertion

Ref	Expression
ttgcontlem1	⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Proof of Theorem ttgcontlem1

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unitssre 13416	. . . . . . . 8 ⊢ (0[,]1) ⊆ ℝ
2		ttgcontlem1.l	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (0[,]1))
3	1, 2	sselid 3942	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℝ)
4		ttgcontlem1.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0[,]1))
5	1, 4	sselid 3942	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℝ)
6	3, 5	remulcld 11185	. . . . . 6 ⊢ (𝜑 → (𝐿 · 𝐾) ∈ ℝ)
7		0re 11157	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		iccssre 13346	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0[,]𝐿) ⊆ ℝ)
9	7, 3, 8	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ ℝ)
10		ttgcontlem1.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
11	9, 10	sseldd 3945	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12	11, 5	remulcld 11185	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℝ)
13	6, 12	resubcld 11583	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ∈ ℝ)
14		1red 11156	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
15	11, 14	remulcld 11185	. . . . . 6 ⊢ (𝜑 → (𝑀 · 1) ∈ ℝ)
16	15, 12	resubcld 11583	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ)
17	11	recnd 11183	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
18		1cnd 11150	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
19	5	recnd 11183	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℂ)
20	17, 18, 19	subdid 11611	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) = ((𝑀 · 1) − (𝑀 · 𝐾)))
21	18, 19	subcld 11512	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℂ)
22		ttgcontlem1.o	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
23		ttgcontlem1.q	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≠ 1)
24	23	necomd 2999	. . . . . . . 8 ⊢ (𝜑 → 1 ≠ 𝐾)
25	18, 19, 24	subne0d 11521	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ≠ 0)
26	17, 21, 22, 25	mulne0d 11807	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ≠ 0)
27	20, 26	eqnetrrd 3012	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ≠ 0)
28	13, 16, 27	redivcld 11983	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ)
29		0xr 11202	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
30	3	rexrd 11205	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ*)
31		iccgelb 13320	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 0 ≤ 𝑀)
32	29, 30, 10, 31	mp3an2i 1466	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
33	11, 32, 22	ne0gt0d 11292	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
34	11, 33	elrpd 12954	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ+)
35	14	rexrd 11205	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ*)
36		iccleub 13319	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 𝐾 ≤ 1)
37	29, 35, 4, 36	mp3an2i 1466	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 1)
38	5, 14, 37, 24	leneltd 11309	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < 1)
39		difrp 12953	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
40	5, 14, 39	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
41	38, 40	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℝ+)
42	34, 41	rpmulcld 12973	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ∈ ℝ+)
43	20, 42	eqeltrrd 2839	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ+)
44	3, 11	resubcld 11583	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℝ)
45		iccleub 13319	. . . . . . . . 9 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 𝑀 ≤ 𝐿)
46	29, 30, 10, 45	mp3an2i 1466	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ≤ 𝐿)
47	3, 11	subge0d 11745	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (𝐿 − 𝑀) ↔ 𝑀 ≤ 𝐿))
48	46, 47	mpbird 256	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (𝐿 − 𝑀))
49		iccgelb 13320	. . . . . . . 8 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 0 ≤ 𝐾)
50	29, 35, 4, 49	mp3an2i 1466	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝐾)
51	44, 5, 48, 50	mulge0d 11732	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((𝐿 − 𝑀) · 𝐾))
52	3	recnd 11183	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
53	52, 17, 19	subdird 11612	. . . . . 6 ⊢ (𝜑 → ((𝐿 − 𝑀) · 𝐾) = ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
54	51, 53	breqtrd 5131	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
55	13, 43, 54	divge0d 12997	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
56		ttgcontlem1.s	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
57		ttgcontlem1.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≠ 0)
58	5, 50, 57	ne0gt0d 11292	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < 𝐾)
59	5, 58	elrpd 12954	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ+)
60	3, 11, 59	lemuldivd 13006	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐾) ≤ 𝑀 ↔ 𝐿 ≤ (𝑀 / 𝐾)))
61	56, 60	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ 𝑀)
62	17	mulid1d 11172	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) = 𝑀)
63	61, 62	breqtrrd 5133	. . . . . . 7 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ (𝑀 · 1))
64	6, 15, 12, 63	lesub1dd 11771	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ ((𝑀 · 1) − (𝑀 · 𝐾)))
65	17, 18	mulcld 11175	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) ∈ ℂ)
66	17, 19	mulcld 11175	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℂ)
67	65, 66	subcld 11512	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℂ)
68	67	mulid1d 11172	. . . . . 6 ⊢ (𝜑 → (((𝑀 · 1) − (𝑀 · 𝐾)) · 1) = ((𝑀 · 1) − (𝑀 · 𝐾)))
69	64, 68	breqtrrd 5133	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1))
70	13, 14, 43	ledivmuld 13010	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1 ↔ ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1)))
71	69, 70	mpbird 256	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1)
72		elicc01 13383	. . . 4 ⊢ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ↔ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ ∧ 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∧ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1))
73	28, 55, 71, 72	syl3anbrc 1343	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1))
74		ttgcontlem1.h	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ℂVec)
75	74	cvsclm 24489	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ ℂMod)
76		ttgbtwnid.2	. . . . . . . 8 ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
77	76, 2	sseldd 3945	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
78		0elunit 13386	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
79		iccss2 13335	. . . . . . . . . 10 ⊢ ((0 ∈ (0[,]1) ∧ 𝐿 ∈ (0[,]1)) → (0[,]𝐿) ⊆ (0[,]1))
80	78, 2, 79	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (0[,]𝐿) ⊆ (0[,]1))
81	80, 76	sstrd 3954	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ 𝑅)
82	81, 10	sseldd 3945	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ 𝑅)
83		eqid 2736	. . . . . . . 8 ⊢ (Scalar‘𝐻) = (Scalar‘𝐻)
84		ttgbtwnid.r	. . . . . . . 8 ⊢ 𝑅 = (Base‘(Scalar‘𝐻))
85	83, 84	clmsubcl 24449	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) ∈ 𝑅)
86	75, 77, 82, 85	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ 𝑅)
87	83, 84	cvsdivcl 24496	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0)) → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
88	74, 86, 82, 22, 87	syl13anc 1372	. . . . 5 ⊢ (𝜑 → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
89	76, 4	sseldd 3945	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑅)
90		1elunit 13387	. . . . . . . . 9 ⊢ 1 ∈ (0[,]1)
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (0[,]1))
92	76, 91	sseldd 3945	. . . . . . 7 ⊢ (𝜑 → 1 ∈ 𝑅)
93	83, 84	clmsubcl 24449	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) ∈ 𝑅)
94	75, 92, 89, 93	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (1 − 𝐾) ∈ 𝑅)
95	83, 84	cvsdivcl 24496	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (1 − 𝐾) ≠ 0)) → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
96	74, 89, 94, 25, 95	syl13anc 1372	. . . . 5 ⊢ (𝜑 → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
97		clmgrp 24431	. . . . . . 7 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ Grp)
98	75, 97	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ Grp)
99		ttgelitv.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
100		ttgelitv.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
101		ttgitvval.b	. . . . . . 7 ⊢ 𝑃 = (Base‘𝐻)
102		ttgitvval.m	. . . . . . 7 ⊢ − = (-g‘𝐻)
103	101, 102	grpsubcl 18827	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝑌 − 𝑋) ∈ 𝑃)
104	98, 99, 100, 103	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ 𝑃)
105		ttgitvval.s	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝐻)
106	101, 83, 105, 84	clmvsass 24452	. . . . 5 ⊢ ((𝐻 ∈ ℂMod ∧ (((𝐿 − 𝑀) / 𝑀) ∈ 𝑅 ∧ (𝐾 / (1 − 𝐾)) ∈ 𝑅 ∧ (𝑌 − 𝑋) ∈ 𝑃)) → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
107	75, 88, 96, 104, 106	syl13anc 1372	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
108	44	recnd 11183	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℂ)
109	108, 17, 19, 21, 22, 25	divmuldivd 11972	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))))
110	53, 20	oveq12d 7375	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
111	109, 110	eqtrd 2776	. . . . 5 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
112	111	oveq1d 7372	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
113		ttgcontlem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
114	101, 102	grpsubcl 18827	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑋 − 𝐴) ∈ 𝑃)
115	98, 100, 113, 114	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ 𝑃)
116		ttgcontlem1.y	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
117	116	oveq2d 7373	. . . . . . . . 9 ⊢ (𝜑 → ((1 − 𝐾) · (𝑋 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
118	19, 21	mulcomd 11176	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 · (1 − 𝐾)) = ((1 − 𝐾) · 𝐾))
119	118	oveq1d 7372	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)))
120	101, 102	grpsubcl 18827	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑌 − 𝐴) ∈ 𝑃)
121	98, 99, 113, 120	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 − 𝐴) ∈ 𝑃)
122	101, 83, 105, 84	clmvsass 24452	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
123	75, 89, 94, 121, 122	syl13anc 1372	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
124	101, 83, 105, 84	clmvsass 24452	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((1 − 𝐾) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
125	75, 94, 89, 121, 124	syl13anc 1372	. . . . . . . . . 10 ⊢ (𝜑 → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
126	119, 123, 125	3eqtr3d 2784	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
127		eqid 2736	. . . . . . . . . . . . 13 ⊢ (-g‘(Scalar‘𝐻)) = (-g‘(Scalar‘𝐻))
128		clmlmod 24430	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ LMod)
129	75, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ LMod)
130	101, 105, 83, 84, 102, 127, 129, 92, 89, 121	lmodsubdir 20380	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
131	83, 84	clmsub 24443	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
132	75, 92, 89, 131	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
133	132	oveq1d 7372	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)))
134	101, 105	clmvs1 24456	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑌 − 𝐴) ∈ 𝑃) → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
135	75, 121, 134	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
136	135	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 − 𝐴) = (1 · (𝑌 − 𝐴)))
137	136, 116	oveq12d 7375	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
138	130, 133, 137	3eqtr4d 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((𝑌 − 𝐴) − (𝑋 − 𝐴)))
139	101, 102	grpnnncan2 18844	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
140	98, 99, 100, 113, 139	syl13anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
141	138, 140	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = (𝑌 − 𝑋))
142	141	oveq2d 7373	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = (𝐾 · (𝑌 − 𝑋)))
143	117, 126, 142	3eqtr2rd 2783	. . . . . . . 8 ⊢ (𝜑 → (𝐾 · (𝑌 − 𝑋)) = ((1 − 𝐾) · (𝑋 − 𝐴)))
144	101, 105, 83, 84, 74, 89, 94, 104, 115, 57, 143	cvsmuleqdivd 24497	. . . . . . 7 ⊢ (𝜑 → (𝑌 − 𝑋) = (((1 − 𝐾) / 𝐾) · (𝑋 − 𝐴)))
145	101, 105, 83, 84, 74, 94, 89, 104, 115, 25, 57, 144	cvsdiveqd 24498	. . . . . 6 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = (𝑋 − 𝐴))
146	145, 115	eqeltrd 2838	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) ∈ 𝑃)
147		ttgcontlem1.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))
148		ttgcontlem1.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ 𝑃)
149	101, 102	grpsubcl 18827	. . . . . . . . . 10 ⊢ ((𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑁 − 𝐴) ∈ 𝑃)
150	98, 148, 113, 149	syl3anc 1371	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − 𝐴) ∈ 𝑃)
151	101, 83, 105, 84	lmodvscl 20339	. . . . . . . . 9 ⊢ ((𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃) → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
152	129, 77, 150, 151	syl3anc 1371	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
153		ttgitvval.p	. . . . . . . . 9 ⊢ + = (+g‘𝐻)
154	101, 153	grpcl 18756	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
155	98, 113, 152, 154	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
156	147, 155	eqeltrd 2838	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
157	101, 102	grpsubcl 18827	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝐵 − 𝑋) ∈ 𝑃)
158	98, 156, 100, 157	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ 𝑃)
159		ttgcontlem1.r	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 𝑀)
160	52, 17, 159	subne0d 11521	. . . . 5 ⊢ (𝜑 → (𝐿 − 𝑀) ≠ 0)
161		ttgcontlem1.x	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
162	161	oveq2d 7373	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑋 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
163	17, 108	mulcomd 11176	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · (𝐿 − 𝑀)) = ((𝐿 − 𝑀) · 𝑀))
164	163	oveq1d 7372	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)))
165	101, 83, 105, 84	clmvsass 24452	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑀 ∈ 𝑅 ∧ (𝐿 − 𝑀) ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
166	75, 82, 86, 150, 165	syl13anc 1372	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
167	101, 83, 105, 84	clmvsass 24452	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
168	75, 86, 82, 150, 167	syl13anc 1372	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
169	164, 166, 168	3eqtr3d 2784	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
170	101, 105, 83, 84, 102, 127, 129, 77, 82, 150	lmodsubdir 20380	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
171	83, 84	clmsub 24443	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
172	75, 77, 82, 171	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
173	172	oveq1d 7372	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)))
174	147	oveq1d 7372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴))
175		lmodabl 20369	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ LMod → 𝐻 ∈ Abel)
176	129, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ Abel)
177	101, 153, 102	ablpncan2 19594	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
178	176, 113, 152, 177	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
179	174, 178	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
180	179, 161	oveq12d 7375	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
181	170, 173, 180	3eqtr4d 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐵 − 𝐴) − (𝑋 − 𝐴)))
182	101, 102	grpnnncan2 18844	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
183	98, 156, 100, 113, 182	syl13anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
184	181, 183	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = (𝐵 − 𝑋))
185	184	oveq2d 7373	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = (𝑀 · (𝐵 − 𝑋)))
186	162, 169, 185	3eqtr2rd 2783	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (𝐵 − 𝑋)) = ((𝐿 − 𝑀) · (𝑋 − 𝐴)))
187	101, 105, 83, 84, 74, 82, 86, 158, 115, 22, 186	cvsmuleqdivd 24497	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑋) = (((𝐿 − 𝑀) / 𝑀) · (𝑋 − 𝐴)))
188	101, 105, 83, 84, 74, 86, 82, 158, 115, 160, 22, 187	cvsdiveqd 24498	. . . . . 6 ⊢ (𝜑 → ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)) = (𝑋 − 𝐴))
189	145, 188	eqtr4d 2779	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)))
190	101, 105, 83, 84, 74, 82, 86, 146, 158, 22, 160, 189	cvsdiveqd 24498	. . . 4 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))) = (𝐵 − 𝑋))
191	107, 112, 190	3eqtr3rd 2785	. . 3 ⊢ (𝜑 → (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
192		oveq1 7364	. . . 4 ⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → (𝑘 · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
193	192	rspceeqv 3595	. . 3 ⊢ (((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ∧ (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))
194	73, 191, 193	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))
195		ttgval.n	. . 3 ⊢ 𝐺 = (toTG‘𝐻)
196		ttgitvval.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
197	195, 196, 101, 102, 105, 100, 99, 74, 156	ttgelitv 27831	. 2 ⊢ (𝜑 → (𝐵 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
198	194, 197	mpbird 256	1 ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073   ⊆ wss 3910   class class class wbr 5105  ‘cfv 6496  (class class class)co 7357  ℝcr 11050  0cc0 11051  1c1 11052   · cmul 11056  ℝ^*cxr 11188   < clt 11189   ≤ cle 11190   − cmin 11385   / cdiv 11812  ℝ⁺crp 12915  [,]cicc 13267  Basecbs 17083  +_gcplusg 17133  Scalarcsca 17136   ·_𝑠 cvsca 17137  Grpcgrp 18748  -_gcsg 18750  Abelcabl 19563  LModclmod 20322  ℂModcclm 24425  ℂVecccvs 24486  Itvcitv 27375  toTGcttg 27815

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-addf 11130  ax-mulf 11131

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-icc 13271  df-fz 13425  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-0g 17323  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751  df-minusg 18752  df-sbg 18753  df-subg 18925  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-dvr 20112  df-drng 20187  df-subrg 20220  df-lmod 20324  df-lvec 20564  df-cnfld 20797  df-clm 24426  df-cvs 24487  df-itv 27377  df-lng 27378  df-ttg 27816

This theorem is referenced by: (None)