Theorem ttgcontlem1 28869

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 13521	. . . . . . . 8 ⊢ (0[,]1) ⊆ ℝ
2		ttgcontlem1.l	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (0[,]1))
3	1, 2	sselid 3961	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℝ)
4		ttgcontlem1.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0[,]1))
5	1, 4	sselid 3961	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℝ)
6	3, 5	remulcld 11270	. . . . . 6 ⊢ (𝜑 → (𝐿 · 𝐾) ∈ ℝ)
7		0re 11242	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		iccssre 13451	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0[,]𝐿) ⊆ ℝ)
9	7, 3, 8	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ ℝ)
10		ttgcontlem1.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
11	9, 10	sseldd 3964	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12	11, 5	remulcld 11270	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℝ)
13	6, 12	resubcld 11670	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ∈ ℝ)
14		1red 11241	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
15	11, 14	remulcld 11270	. . . . . 6 ⊢ (𝜑 → (𝑀 · 1) ∈ ℝ)
16	15, 12	resubcld 11670	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ)
17	11	recnd 11268	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
18		1cnd 11235	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
19	5	recnd 11268	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℂ)
20	17, 18, 19	subdid 11698	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) = ((𝑀 · 1) − (𝑀 · 𝐾)))
21	18, 19	subcld 11599	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℂ)
22		ttgcontlem1.o	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
23		ttgcontlem1.q	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≠ 1)
24	23	necomd 2988	. . . . . . . 8 ⊢ (𝜑 → 1 ≠ 𝐾)
25	18, 19, 24	subne0d 11608	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ≠ 0)
26	17, 21, 22, 25	mulne0d 11894	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ≠ 0)
27	20, 26	eqnetrrd 3001	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ≠ 0)
28	13, 16, 27	redivcld 12074	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ)
29		0xr 11287	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
30	3	rexrd 11290	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ*)
31		iccgelb 13424	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 0 ≤ 𝑀)
32	29, 30, 10, 31	mp3an2i 1468	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
33	11, 32, 22	ne0gt0d 11377	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
34	11, 33	elrpd 13053	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ+)
35	14	rexrd 11290	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ*)
36		iccleub 13423	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 𝐾 ≤ 1)
37	29, 35, 4, 36	mp3an2i 1468	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 1)
38	5, 14, 37, 24	leneltd 11394	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < 1)
39		difrp 13052	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
40	5, 14, 39	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
41	38, 40	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℝ+)
42	34, 41	rpmulcld 13072	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ∈ ℝ+)
43	20, 42	eqeltrrd 2836	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ+)
44	3, 11	resubcld 11670	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℝ)
45		iccleub 13423	. . . . . . . . 9 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 𝑀 ≤ 𝐿)
46	29, 30, 10, 45	mp3an2i 1468	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ≤ 𝐿)
47	3, 11	subge0d 11832	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (𝐿 − 𝑀) ↔ 𝑀 ≤ 𝐿))
48	46, 47	mpbird 257	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (𝐿 − 𝑀))
49		iccgelb 13424	. . . . . . . 8 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 0 ≤ 𝐾)
50	29, 35, 4, 49	mp3an2i 1468	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝐾)
51	44, 5, 48, 50	mulge0d 11819	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((𝐿 − 𝑀) · 𝐾))
52	3	recnd 11268	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
53	52, 17, 19	subdird 11699	. . . . . 6 ⊢ (𝜑 → ((𝐿 − 𝑀) · 𝐾) = ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
54	51, 53	breqtrd 5150	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
55	13, 43, 54	divge0d 13096	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
56		ttgcontlem1.s	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
57		ttgcontlem1.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≠ 0)
58	5, 50, 57	ne0gt0d 11377	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < 𝐾)
59	5, 58	elrpd 13053	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ+)
60	3, 11, 59	lemuldivd 13105	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐾) ≤ 𝑀 ↔ 𝐿 ≤ (𝑀 / 𝐾)))
61	56, 60	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ 𝑀)
62	17	mulridd 11257	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) = 𝑀)
63	61, 62	breqtrrd 5152	. . . . . . 7 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ (𝑀 · 1))
64	6, 15, 12, 63	lesub1dd 11858	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ ((𝑀 · 1) − (𝑀 · 𝐾)))
65	17, 18	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) ∈ ℂ)
66	17, 19	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℂ)
67	65, 66	subcld 11599	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℂ)
68	67	mulridd 11257	. . . . . 6 ⊢ (𝜑 → (((𝑀 · 1) − (𝑀 · 𝐾)) · 1) = ((𝑀 · 1) − (𝑀 · 𝐾)))
69	64, 68	breqtrrd 5152	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1))
70	13, 14, 43	ledivmuld 13109	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1 ↔ ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1)))
71	69, 70	mpbird 257	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1)
72		elicc01 13488	. . . 4 ⊢ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ↔ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ ∧ 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∧ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1))
73	28, 55, 71, 72	syl3anbrc 1344	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1))
74		ttgcontlem1.h	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ℂVec)
75	74	cvsclm 25082	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ ℂMod)
76		ttgbtwnid.2	. . . . . . . 8 ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
77	76, 2	sseldd 3964	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
78		0elunit 13491	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
79		iccss2 13439	. . . . . . . . . 10 ⊢ ((0 ∈ (0[,]1) ∧ 𝐿 ∈ (0[,]1)) → (0[,]𝐿) ⊆ (0[,]1))
80	78, 2, 79	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (0[,]𝐿) ⊆ (0[,]1))
81	80, 76	sstrd 3974	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ 𝑅)
82	81, 10	sseldd 3964	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ 𝑅)
83		eqid 2736	. . . . . . . 8 ⊢ (Scalar‘𝐻) = (Scalar‘𝐻)
84		ttgbtwnid.r	. . . . . . . 8 ⊢ 𝑅 = (Base‘(Scalar‘𝐻))
85	83, 84	clmsubcl 25042	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) ∈ 𝑅)
86	75, 77, 82, 85	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ 𝑅)
87	83, 84	cvsdivcl 25089	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0)) → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
88	74, 86, 82, 22, 87	syl13anc 1374	. . . . 5 ⊢ (𝜑 → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
89	76, 4	sseldd 3964	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑅)
90		1elunit 13492	. . . . . . . . 9 ⊢ 1 ∈ (0[,]1)
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (0[,]1))
92	76, 91	sseldd 3964	. . . . . . 7 ⊢ (𝜑 → 1 ∈ 𝑅)
93	83, 84	clmsubcl 25042	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) ∈ 𝑅)
94	75, 92, 89, 93	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (1 − 𝐾) ∈ 𝑅)
95	83, 84	cvsdivcl 25089	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (1 − 𝐾) ≠ 0)) → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
96	74, 89, 94, 25, 95	syl13anc 1374	. . . . 5 ⊢ (𝜑 → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
97		clmgrp 25024	. . . . . . 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 19008	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝑌 − 𝑋) ∈ 𝑃)
104	98, 99, 100, 103	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ 𝑃)
105		ttgitvval.s	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝐻)
106	101, 83, 105, 84	clmvsass 25045	. . . . 5 ⊢ ((𝐻 ∈ ℂMod ∧ (((𝐿 − 𝑀) / 𝑀) ∈ 𝑅 ∧ (𝐾 / (1 − 𝐾)) ∈ 𝑅 ∧ (𝑌 − 𝑋) ∈ 𝑃)) → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
107	75, 88, 96, 104, 106	syl13anc 1374	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
108	44	recnd 11268	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℂ)
109	108, 17, 19, 21, 22, 25	divmuldivd 12063	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))))
110	53, 20	oveq12d 7428	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
111	109, 110	eqtrd 2771	. . . . 5 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
112	111	oveq1d 7425	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
113		ttgcontlem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
114	101, 102	grpsubcl 19008	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑋 − 𝐴) ∈ 𝑃)
115	98, 100, 113, 114	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ 𝑃)
116		ttgcontlem1.y	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
117	116	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → ((1 − 𝐾) · (𝑋 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
118	19, 21	mulcomd 11261	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 · (1 − 𝐾)) = ((1 − 𝐾) · 𝐾))
119	118	oveq1d 7425	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)))
120	101, 102	grpsubcl 19008	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑌 − 𝐴) ∈ 𝑃)
121	98, 99, 113, 120	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 − 𝐴) ∈ 𝑃)
122	101, 83, 105, 84	clmvsass 25045	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
123	75, 89, 94, 121, 122	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
124	101, 83, 105, 84	clmvsass 25045	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((1 − 𝐾) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
125	75, 94, 89, 121, 124	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
126	119, 123, 125	3eqtr3d 2779	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
127		eqid 2736	. . . . . . . . . . . . 13 ⊢ (-g‘(Scalar‘𝐻)) = (-g‘(Scalar‘𝐻))
128		clmlmod 25023	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ LMod)
129	75, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ LMod)
130	101, 105, 83, 84, 102, 127, 129, 92, 89, 121	lmodsubdir 20882	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
131	83, 84	clmsub 25036	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
132	75, 92, 89, 131	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
133	132	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)))
134	101, 105	clmvs1 25049	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑌 − 𝐴) ∈ 𝑃) → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
135	75, 121, 134	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
136	135	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 − 𝐴) = (1 · (𝑌 − 𝐴)))
137	136, 116	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
138	130, 133, 137	3eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((𝑌 − 𝐴) − (𝑋 − 𝐴)))
139	101, 102	grpnnncan2 19025	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
140	98, 99, 100, 113, 139	syl13anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
141	138, 140	eqtrd 2771	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = (𝑌 − 𝑋))
142	141	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = (𝐾 · (𝑌 − 𝑋)))
143	117, 126, 142	3eqtr2rd 2778	. . . . . . . 8 ⊢ (𝜑 → (𝐾 · (𝑌 − 𝑋)) = ((1 − 𝐾) · (𝑋 − 𝐴)))
144	101, 105, 83, 84, 74, 89, 94, 104, 115, 57, 143	cvsmuleqdivd 25090	. . . . . . 7 ⊢ (𝜑 → (𝑌 − 𝑋) = (((1 − 𝐾) / 𝐾) · (𝑋 − 𝐴)))
145	101, 105, 83, 84, 74, 94, 89, 104, 115, 25, 57, 144	cvsdiveqd 25091	. . . . . 6 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = (𝑋 − 𝐴))
146	145, 115	eqeltrd 2835	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) ∈ 𝑃)
147		ttgcontlem1.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))
148		ttgcontlem1.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ 𝑃)
149	101, 102	grpsubcl 19008	. . . . . . . . . 10 ⊢ ((𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑁 − 𝐴) ∈ 𝑃)
150	98, 148, 113, 149	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − 𝐴) ∈ 𝑃)
151	101, 83, 105, 84	lmodvscl 20840	. . . . . . . . 9 ⊢ ((𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃) → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
152	129, 77, 150, 151	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
153		ttgitvval.p	. . . . . . . . 9 ⊢ + = (+g‘𝐻)
154	101, 153	grpcl 18929	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
155	98, 113, 152, 154	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
156	147, 155	eqeltrd 2835	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
157	101, 102	grpsubcl 19008	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝐵 − 𝑋) ∈ 𝑃)
158	98, 156, 100, 157	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ 𝑃)
159		ttgcontlem1.r	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 𝑀)
160	52, 17, 159	subne0d 11608	. . . . 5 ⊢ (𝜑 → (𝐿 − 𝑀) ≠ 0)
161		ttgcontlem1.x	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
162	161	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑋 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
163	17, 108	mulcomd 11261	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · (𝐿 − 𝑀)) = ((𝐿 − 𝑀) · 𝑀))
164	163	oveq1d 7425	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)))
165	101, 83, 105, 84	clmvsass 25045	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑀 ∈ 𝑅 ∧ (𝐿 − 𝑀) ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
166	75, 82, 86, 150, 165	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
167	101, 83, 105, 84	clmvsass 25045	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
168	75, 86, 82, 150, 167	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
169	164, 166, 168	3eqtr3d 2779	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
170	101, 105, 83, 84, 102, 127, 129, 77, 82, 150	lmodsubdir 20882	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
171	83, 84	clmsub 25036	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
172	75, 77, 82, 171	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
173	172	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)))
174	147	oveq1d 7425	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴))
175		lmodabl 20871	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ LMod → 𝐻 ∈ Abel)
176	129, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ Abel)
177	101, 153, 102	ablpncan2 19801	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
178	176, 113, 152, 177	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
179	174, 178	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
180	179, 161	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
181	170, 173, 180	3eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐵 − 𝐴) − (𝑋 − 𝐴)))
182	101, 102	grpnnncan2 19025	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
183	98, 156, 100, 113, 182	syl13anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
184	181, 183	eqtrd 2771	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = (𝐵 − 𝑋))
185	184	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = (𝑀 · (𝐵 − 𝑋)))
186	162, 169, 185	3eqtr2rd 2778	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (𝐵 − 𝑋)) = ((𝐿 − 𝑀) · (𝑋 − 𝐴)))
187	101, 105, 83, 84, 74, 82, 86, 158, 115, 22, 186	cvsmuleqdivd 25090	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑋) = (((𝐿 − 𝑀) / 𝑀) · (𝑋 − 𝐴)))
188	101, 105, 83, 84, 74, 86, 82, 158, 115, 160, 22, 187	cvsdiveqd 25091	. . . . . 6 ⊢ (𝜑 → ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)) = (𝑋 − 𝐴))
189	145, 188	eqtr4d 2774	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)))
190	101, 105, 83, 84, 74, 82, 86, 146, 158, 22, 160, 189	cvsdiveqd 25091	. . . 4 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))) = (𝐵 − 𝑋))
191	107, 112, 190	3eqtr3rd 2780	. . 3 ⊢ (𝜑 → (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
192		oveq1 7417	. . . 4 ⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → (𝑘 · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
193	192	rspceeqv 3629	. . 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 28867	. 2 ⊢ (𝜑 → (𝐵 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
198	194, 197	mpbird 257	1 ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∃wrex 3061   ⊆ wss 3931   class class class wbr 5124  ‘cfv 6536  (class class class)co 7410  ℝcr 11133  0cc0 11134  1c1 11135   · cmul 11139  ℝ^*cxr 11273   < clt 11274   ≤ cle 11275   − cmin 11471   / cdiv 11899  ℝ⁺crp 13013  [,]cicc 13370  Basecbs 17233  +_gcplusg 17276  Scalarcsca 17279   ·_𝑠 cvsca 17280  Grpcgrp 18921  -_gcsg 18923  Abelcabl 19767  LModclmod 20822  ℂModcclm 25018  ℂVecccvs 25079  Itvcitv 28417  toTGcttg 28857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-addf 11213  ax-mulf 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-tpos 8230  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12507  df-z 12594  df-dec 12714  df-uz 12858  df-rp 13014  df-icc 13374  df-fz 13530  df-struct 17171  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17234  df-ress 17257  df-plusg 17289  df-mulr 17290  df-starv 17291  df-tset 17295  df-ple 17296  df-ds 17298  df-unif 17299  df-0g 17460  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-grp 18924  df-minusg 18925  df-sbg 18926  df-subg 19111  df-cmn 19768  df-abl 19769  df-mgp 20106  df-rng 20118  df-ur 20147  df-ring 20200  df-cring 20201  df-oppr 20302  df-dvdsr 20322  df-unit 20323  df-invr 20353  df-dvr 20366  df-subrg 20535  df-drng 20696  df-lmod 20824  df-lvec 21066  df-cnfld 21321  df-clm 25019  df-cvs 25080  df-itv 28419  df-lng 28420  df-ttg 28858

This theorem is referenced by: (None)