Theorem ttgcontlem1 27252

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 13231	. . . . . . . 8 ⊢ (0[,]1) ⊆ ℝ
2		ttgcontlem1.l	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (0[,]1))
3	1, 2	sselid 3919	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℝ)
4		ttgcontlem1.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0[,]1))
5	1, 4	sselid 3919	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℝ)
6	3, 5	remulcld 11005	. . . . . 6 ⊢ (𝜑 → (𝐿 · 𝐾) ∈ ℝ)
7		0re 10977	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		iccssre 13161	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0[,]𝐿) ⊆ ℝ)
9	7, 3, 8	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ ℝ)
10		ttgcontlem1.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
11	9, 10	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12	11, 5	remulcld 11005	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℝ)
13	6, 12	resubcld 11403	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ∈ ℝ)
14		1red 10976	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
15	11, 14	remulcld 11005	. . . . . 6 ⊢ (𝜑 → (𝑀 · 1) ∈ ℝ)
16	15, 12	resubcld 11403	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ)
17	11	recnd 11003	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
18		1cnd 10970	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
19	5	recnd 11003	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℂ)
20	17, 18, 19	subdid 11431	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) = ((𝑀 · 1) − (𝑀 · 𝐾)))
21	18, 19	subcld 11332	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℂ)
22		ttgcontlem1.o	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
23		ttgcontlem1.q	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≠ 1)
24	23	necomd 2999	. . . . . . . 8 ⊢ (𝜑 → 1 ≠ 𝐾)
25	18, 19, 24	subne0d 11341	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ≠ 0)
26	17, 21, 22, 25	mulne0d 11627	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ≠ 0)
27	20, 26	eqnetrrd 3012	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ≠ 0)
28	13, 16, 27	redivcld 11803	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ)
29		0xr 11022	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
30	3	rexrd 11025	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ*)
31		iccgelb 13135	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 0 ≤ 𝑀)
32	29, 30, 10, 31	mp3an2i 1465	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
33	11, 32, 22	ne0gt0d 11112	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
34	11, 33	elrpd 12769	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ+)
35	14	rexrd 11025	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ*)
36		iccleub 13134	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 𝐾 ≤ 1)
37	29, 35, 4, 36	mp3an2i 1465	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 1)
38	5, 14, 37, 24	leneltd 11129	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < 1)
39		difrp 12768	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
40	5, 14, 39	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
41	38, 40	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℝ+)
42	34, 41	rpmulcld 12788	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ∈ ℝ+)
43	20, 42	eqeltrrd 2840	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ+)
44	3, 11	resubcld 11403	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℝ)
45		iccleub 13134	. . . . . . . . 9 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 𝑀 ≤ 𝐿)
46	29, 30, 10, 45	mp3an2i 1465	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ≤ 𝐿)
47	3, 11	subge0d 11565	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (𝐿 − 𝑀) ↔ 𝑀 ≤ 𝐿))
48	46, 47	mpbird 256	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (𝐿 − 𝑀))
49		iccgelb 13135	. . . . . . . 8 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 0 ≤ 𝐾)
50	29, 35, 4, 49	mp3an2i 1465	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝐾)
51	44, 5, 48, 50	mulge0d 11552	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((𝐿 − 𝑀) · 𝐾))
52	3	recnd 11003	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
53	52, 17, 19	subdird 11432	. . . . . 6 ⊢ (𝜑 → ((𝐿 − 𝑀) · 𝐾) = ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
54	51, 53	breqtrd 5100	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
55	13, 43, 54	divge0d 12812	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
56		ttgcontlem1.s	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
57		ttgcontlem1.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≠ 0)
58	5, 50, 57	ne0gt0d 11112	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < 𝐾)
59	5, 58	elrpd 12769	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ+)
60	3, 11, 59	lemuldivd 12821	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐾) ≤ 𝑀 ↔ 𝐿 ≤ (𝑀 / 𝐾)))
61	56, 60	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ 𝑀)
62	17	mulid1d 10992	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) = 𝑀)
63	61, 62	breqtrrd 5102	. . . . . . 7 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ (𝑀 · 1))
64	6, 15, 12, 63	lesub1dd 11591	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ ((𝑀 · 1) − (𝑀 · 𝐾)))
65	17, 18	mulcld 10995	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) ∈ ℂ)
66	17, 19	mulcld 10995	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℂ)
67	65, 66	subcld 11332	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℂ)
68	67	mulid1d 10992	. . . . . 6 ⊢ (𝜑 → (((𝑀 · 1) − (𝑀 · 𝐾)) · 1) = ((𝑀 · 1) − (𝑀 · 𝐾)))
69	64, 68	breqtrrd 5102	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1))
70	13, 14, 43	ledivmuld 12825	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1 ↔ ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1)))
71	69, 70	mpbird 256	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1)
72		elicc01 13198	. . . 4 ⊢ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ↔ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ ∧ 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∧ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1))
73	28, 55, 71, 72	syl3anbrc 1342	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1))
74		ttgcontlem1.h	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ℂVec)
75	74	cvsclm 24289	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ ℂMod)
76		ttgbtwnid.2	. . . . . . . 8 ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
77	76, 2	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
78		0elunit 13201	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
79		iccss2 13150	. . . . . . . . . 10 ⊢ ((0 ∈ (0[,]1) ∧ 𝐿 ∈ (0[,]1)) → (0[,]𝐿) ⊆ (0[,]1))
80	78, 2, 79	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (0[,]𝐿) ⊆ (0[,]1))
81	80, 76	sstrd 3931	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ 𝑅)
82	81, 10	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ 𝑅)
83		eqid 2738	. . . . . . . 8 ⊢ (Scalar‘𝐻) = (Scalar‘𝐻)
84		ttgbtwnid.r	. . . . . . . 8 ⊢ 𝑅 = (Base‘(Scalar‘𝐻))
85	83, 84	clmsubcl 24249	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) ∈ 𝑅)
86	75, 77, 82, 85	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ 𝑅)
87	83, 84	cvsdivcl 24296	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0)) → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
88	74, 86, 82, 22, 87	syl13anc 1371	. . . . 5 ⊢ (𝜑 → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
89	76, 4	sseldd 3922	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑅)
90		1elunit 13202	. . . . . . . . 9 ⊢ 1 ∈ (0[,]1)
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (0[,]1))
92	76, 91	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 1 ∈ 𝑅)
93	83, 84	clmsubcl 24249	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) ∈ 𝑅)
94	75, 92, 89, 93	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → (1 − 𝐾) ∈ 𝑅)
95	83, 84	cvsdivcl 24296	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (1 − 𝐾) ≠ 0)) → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
96	74, 89, 94, 25, 95	syl13anc 1371	. . . . 5 ⊢ (𝜑 → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
97		clmgrp 24231	. . . . . . 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 18655	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝑌 − 𝑋) ∈ 𝑃)
104	98, 99, 100, 103	syl3anc 1370	. . . . 5 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ 𝑃)
105		ttgitvval.s	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝐻)
106	101, 83, 105, 84	clmvsass 24252	. . . . 5 ⊢ ((𝐻 ∈ ℂMod ∧ (((𝐿 − 𝑀) / 𝑀) ∈ 𝑅 ∧ (𝐾 / (1 − 𝐾)) ∈ 𝑅 ∧ (𝑌 − 𝑋) ∈ 𝑃)) → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
107	75, 88, 96, 104, 106	syl13anc 1371	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
108	44	recnd 11003	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℂ)
109	108, 17, 19, 21, 22, 25	divmuldivd 11792	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))))
110	53, 20	oveq12d 7293	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
111	109, 110	eqtrd 2778	. . . . 5 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
112	111	oveq1d 7290	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
113		ttgcontlem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
114	101, 102	grpsubcl 18655	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑋 − 𝐴) ∈ 𝑃)
115	98, 100, 113, 114	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ 𝑃)
116		ttgcontlem1.y	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
117	116	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → ((1 − 𝐾) · (𝑋 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
118	19, 21	mulcomd 10996	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 · (1 − 𝐾)) = ((1 − 𝐾) · 𝐾))
119	118	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)))
120	101, 102	grpsubcl 18655	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑌 − 𝐴) ∈ 𝑃)
121	98, 99, 113, 120	syl3anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 − 𝐴) ∈ 𝑃)
122	101, 83, 105, 84	clmvsass 24252	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
123	75, 89, 94, 121, 122	syl13anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
124	101, 83, 105, 84	clmvsass 24252	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((1 − 𝐾) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
125	75, 94, 89, 121, 124	syl13anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
126	119, 123, 125	3eqtr3d 2786	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
127		eqid 2738	. . . . . . . . . . . . 13 ⊢ (-g‘(Scalar‘𝐻)) = (-g‘(Scalar‘𝐻))
128		clmlmod 24230	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ LMod)
129	75, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ LMod)
130	101, 105, 83, 84, 102, 127, 129, 92, 89, 121	lmodsubdir 20181	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
131	83, 84	clmsub 24243	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
132	75, 92, 89, 131	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
133	132	oveq1d 7290	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)))
134	101, 105	clmvs1 24256	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑌 − 𝐴) ∈ 𝑃) → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
135	75, 121, 134	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
136	135	eqcomd 2744	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 − 𝐴) = (1 · (𝑌 − 𝐴)))
137	136, 116	oveq12d 7293	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
138	130, 133, 137	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((𝑌 − 𝐴) − (𝑋 − 𝐴)))
139	101, 102	grpnnncan2 18672	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
140	98, 99, 100, 113, 139	syl13anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
141	138, 140	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = (𝑌 − 𝑋))
142	141	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = (𝐾 · (𝑌 − 𝑋)))
143	117, 126, 142	3eqtr2rd 2785	. . . . . . . 8 ⊢ (𝜑 → (𝐾 · (𝑌 − 𝑋)) = ((1 − 𝐾) · (𝑋 − 𝐴)))
144	101, 105, 83, 84, 74, 89, 94, 104, 115, 57, 143	cvsmuleqdivd 24297	. . . . . . 7 ⊢ (𝜑 → (𝑌 − 𝑋) = (((1 − 𝐾) / 𝐾) · (𝑋 − 𝐴)))
145	101, 105, 83, 84, 74, 94, 89, 104, 115, 25, 57, 144	cvsdiveqd 24298	. . . . . 6 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = (𝑋 − 𝐴))
146	145, 115	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) ∈ 𝑃)
147		ttgcontlem1.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))
148		ttgcontlem1.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ 𝑃)
149	101, 102	grpsubcl 18655	. . . . . . . . . 10 ⊢ ((𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑁 − 𝐴) ∈ 𝑃)
150	98, 148, 113, 149	syl3anc 1370	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − 𝐴) ∈ 𝑃)
151	101, 83, 105, 84	lmodvscl 20140	. . . . . . . . 9 ⊢ ((𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃) → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
152	129, 77, 150, 151	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
153		ttgitvval.p	. . . . . . . . 9 ⊢ + = (+g‘𝐻)
154	101, 153	grpcl 18585	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
155	98, 113, 152, 154	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
156	147, 155	eqeltrd 2839	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
157	101, 102	grpsubcl 18655	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝐵 − 𝑋) ∈ 𝑃)
158	98, 156, 100, 157	syl3anc 1370	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ 𝑃)
159		ttgcontlem1.r	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 𝑀)
160	52, 17, 159	subne0d 11341	. . . . 5 ⊢ (𝜑 → (𝐿 − 𝑀) ≠ 0)
161		ttgcontlem1.x	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
162	161	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑋 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
163	17, 108	mulcomd 10996	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · (𝐿 − 𝑀)) = ((𝐿 − 𝑀) · 𝑀))
164	163	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)))
165	101, 83, 105, 84	clmvsass 24252	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑀 ∈ 𝑅 ∧ (𝐿 − 𝑀) ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
166	75, 82, 86, 150, 165	syl13anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
167	101, 83, 105, 84	clmvsass 24252	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
168	75, 86, 82, 150, 167	syl13anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
169	164, 166, 168	3eqtr3d 2786	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
170	101, 105, 83, 84, 102, 127, 129, 77, 82, 150	lmodsubdir 20181	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
171	83, 84	clmsub 24243	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
172	75, 77, 82, 171	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
173	172	oveq1d 7290	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)))
174	147	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴))
175		lmodabl 20170	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ LMod → 𝐻 ∈ Abel)
176	129, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ Abel)
177	101, 153, 102	ablpncan2 19417	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
178	176, 113, 152, 177	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
179	174, 178	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
180	179, 161	oveq12d 7293	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
181	170, 173, 180	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐵 − 𝐴) − (𝑋 − 𝐴)))
182	101, 102	grpnnncan2 18672	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
183	98, 156, 100, 113, 182	syl13anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
184	181, 183	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = (𝐵 − 𝑋))
185	184	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = (𝑀 · (𝐵 − 𝑋)))
186	162, 169, 185	3eqtr2rd 2785	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (𝐵 − 𝑋)) = ((𝐿 − 𝑀) · (𝑋 − 𝐴)))
187	101, 105, 83, 84, 74, 82, 86, 158, 115, 22, 186	cvsmuleqdivd 24297	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑋) = (((𝐿 − 𝑀) / 𝑀) · (𝑋 − 𝐴)))
188	101, 105, 83, 84, 74, 86, 82, 158, 115, 160, 22, 187	cvsdiveqd 24298	. . . . . 6 ⊢ (𝜑 → ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)) = (𝑋 − 𝐴))
189	145, 188	eqtr4d 2781	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)))
190	101, 105, 83, 84, 74, 82, 86, 146, 158, 22, 160, 189	cvsdiveqd 24298	. . . 4 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))) = (𝐵 − 𝑋))
191	107, 112, 190	3eqtr3rd 2787	. . 3 ⊢ (𝜑 → (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
192		oveq1 7282	. . . 4 ⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → (𝑘 · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
193	192	rspceeqv 3575	. . 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 27250	. 2 ⊢ (𝜑 → (𝐵 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
198	194, 197	mpbird 256	1 ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3065   ⊆ wss 3887   class class class wbr 5074  ‘cfv 6433  (class class class)co 7275  ℝcr 10870  0cc0 10871  1c1 10872   · cmul 10876  ℝ^*cxr 11008   < clt 11009   ≤ cle 11010   − cmin 11205   / cdiv 11632  ℝ⁺crp 12730  [,]cicc 13082  Basecbs 16912  +_gcplusg 16962  Scalarcsca 16965   ·_𝑠 cvsca 16966  Grpcgrp 18577  -_gcsg 18579  Abelcabl 19387  LModclmod 20123  ℂModcclm 24225  ℂVecccvs 24286  Itvcitv 26794  toTGcttg 27234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-addf 10950  ax-mulf 10951

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-tpos 8042  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-rp 12731  df-icc 13086  df-fz 13240  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-0g 17152  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-grp 18580  df-minusg 18581  df-sbg 18582  df-subg 18752  df-cmn 19388  df-abl 19389  df-mgp 19721  df-ur 19738  df-ring 19785  df-cring 19786  df-oppr 19862  df-dvdsr 19883  df-unit 19884  df-invr 19914  df-dvr 19925  df-drng 19993  df-subrg 20022  df-lmod 20125  df-lvec 20365  df-cnfld 20598  df-clm 24226  df-cvs 24287  df-itv 26796  df-lng 26797  df-ttg 27235

This theorem is referenced by: (None)