Theorem ttgcontlem1 28969

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 13427	. . . . . . . 8 ⊢ (0[,]1) ⊆ ℝ
2		ttgcontlem1.l	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (0[,]1))
3	1, 2	sselid 3933	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℝ)
4		ttgcontlem1.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0[,]1))
5	1, 4	sselid 3933	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℝ)
6	3, 5	remulcld 11174	. . . . . 6 ⊢ (𝜑 → (𝐿 · 𝐾) ∈ ℝ)
7		0re 11146	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		iccssre 13357	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0[,]𝐿) ⊆ ℝ)
9	7, 3, 8	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ ℝ)
10		ttgcontlem1.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
11	9, 10	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12	11, 5	remulcld 11174	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℝ)
13	6, 12	resubcld 11577	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ∈ ℝ)
14		1red 11145	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
15	11, 14	remulcld 11174	. . . . . 6 ⊢ (𝜑 → (𝑀 · 1) ∈ ℝ)
16	15, 12	resubcld 11577	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ)
17	11	recnd 11172	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
18		1cnd 11139	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
19	5	recnd 11172	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℂ)
20	17, 18, 19	subdid 11605	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) = ((𝑀 · 1) − (𝑀 · 𝐾)))
21	18, 19	subcld 11504	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℂ)
22		ttgcontlem1.o	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
23		ttgcontlem1.q	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≠ 1)
24	23	necomd 2988	. . . . . . . 8 ⊢ (𝜑 → 1 ≠ 𝐾)
25	18, 19, 24	subne0d 11513	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ≠ 0)
26	17, 21, 22, 25	mulne0d 11801	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ≠ 0)
27	20, 26	eqnetrrd 3001	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ≠ 0)
28	13, 16, 27	redivcld 11981	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ)
29		0xr 11191	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
30	3	rexrd 11194	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ*)
31		iccgelb 13330	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 0 ≤ 𝑀)
32	29, 30, 10, 31	mp3an2i 1469	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
33	11, 32, 22	ne0gt0d 11282	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
34	11, 33	elrpd 12958	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ+)
35	14	rexrd 11194	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ*)
36		iccleub 13329	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 𝐾 ≤ 1)
37	29, 35, 4, 36	mp3an2i 1469	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 1)
38	5, 14, 37, 24	leneltd 11299	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < 1)
39		difrp 12957	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
40	5, 14, 39	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ+))
41	38, 40	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℝ+)
42	34, 41	rpmulcld 12977	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ∈ ℝ+)
43	20, 42	eqeltrrd 2838	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ+)
44	3, 11	resubcld 11577	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℝ)
45		iccleub 13329	. . . . . . . . 9 ⊢ ((0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 𝑀 ≤ 𝐿)
46	29, 30, 10, 45	mp3an2i 1469	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ≤ 𝐿)
47	3, 11	subge0d 11739	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (𝐿 − 𝑀) ↔ 𝑀 ≤ 𝐿))
48	46, 47	mpbird 257	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (𝐿 − 𝑀))
49		iccgelb 13330	. . . . . . . 8 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 0 ≤ 𝐾)
50	29, 35, 4, 49	mp3an2i 1469	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝐾)
51	44, 5, 48, 50	mulge0d 11726	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((𝐿 − 𝑀) · 𝐾))
52	3	recnd 11172	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
53	52, 17, 19	subdird 11606	. . . . . 6 ⊢ (𝜑 → ((𝐿 − 𝑀) · 𝐾) = ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
54	51, 53	breqtrd 5126	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
55	13, 43, 54	divge0d 13001	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
56		ttgcontlem1.s	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
57		ttgcontlem1.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≠ 0)
58	5, 50, 57	ne0gt0d 11282	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < 𝐾)
59	5, 58	elrpd 12958	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ+)
60	3, 11, 59	lemuldivd 13010	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐾) ≤ 𝑀 ↔ 𝐿 ≤ (𝑀 / 𝐾)))
61	56, 60	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ 𝑀)
62	17	mulridd 11161	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) = 𝑀)
63	61, 62	breqtrrd 5128	. . . . . . 7 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ (𝑀 · 1))
64	6, 15, 12, 63	lesub1dd 11765	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ ((𝑀 · 1) − (𝑀 · 𝐾)))
65	17, 18	mulcld 11164	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) ∈ ℂ)
66	17, 19	mulcld 11164	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℂ)
67	65, 66	subcld 11504	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℂ)
68	67	mulridd 11161	. . . . . 6 ⊢ (𝜑 → (((𝑀 · 1) − (𝑀 · 𝐾)) · 1) = ((𝑀 · 1) − (𝑀 · 𝐾)))
69	64, 68	breqtrrd 5128	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1))
70	13, 14, 43	ledivmuld 13014	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1 ↔ ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1)))
71	69, 70	mpbird 257	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1)
72		elicc01 13394	. . . 4 ⊢ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ↔ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ ∧ 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∧ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1))
73	28, 55, 71, 72	syl3anbrc 1345	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1))
74		ttgcontlem1.h	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ℂVec)
75	74	cvsclm 25094	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ ℂMod)
76		ttgbtwnid.2	. . . . . . . 8 ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
77	76, 2	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
78		0elunit 13397	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
79		iccss2 13345	. . . . . . . . . 10 ⊢ ((0 ∈ (0[,]1) ∧ 𝐿 ∈ (0[,]1)) → (0[,]𝐿) ⊆ (0[,]1))
80	78, 2, 79	sylancr 588	. . . . . . . . 9 ⊢ (𝜑 → (0[,]𝐿) ⊆ (0[,]1))
81	80, 76	sstrd 3946	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ 𝑅)
82	81, 10	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ 𝑅)
83		eqid 2737	. . . . . . . 8 ⊢ (Scalar‘𝐻) = (Scalar‘𝐻)
84		ttgbtwnid.r	. . . . . . . 8 ⊢ 𝑅 = (Base‘(Scalar‘𝐻))
85	83, 84	clmsubcl 25054	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) ∈ 𝑅)
86	75, 77, 82, 85	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ 𝑅)
87	83, 84	cvsdivcl 25101	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0)) → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
88	74, 86, 82, 22, 87	syl13anc 1375	. . . . 5 ⊢ (𝜑 → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
89	76, 4	sseldd 3936	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑅)
90		1elunit 13398	. . . . . . . . 9 ⊢ 1 ∈ (0[,]1)
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (0[,]1))
92	76, 91	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 1 ∈ 𝑅)
93	83, 84	clmsubcl 25054	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) ∈ 𝑅)
94	75, 92, 89, 93	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → (1 − 𝐾) ∈ 𝑅)
95	83, 84	cvsdivcl 25101	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (1 − 𝐾) ≠ 0)) → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
96	74, 89, 94, 25, 95	syl13anc 1375	. . . . 5 ⊢ (𝜑 → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
97		clmgrp 25036	. . . . . . 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 18962	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝑌 − 𝑋) ∈ 𝑃)
104	98, 99, 100, 103	syl3anc 1374	. . . . 5 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ 𝑃)
105		ttgitvval.s	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝐻)
106	101, 83, 105, 84	clmvsass 25057	. . . . 5 ⊢ ((𝐻 ∈ ℂMod ∧ (((𝐿 − 𝑀) / 𝑀) ∈ 𝑅 ∧ (𝐾 / (1 − 𝐾)) ∈ 𝑅 ∧ (𝑌 − 𝑋) ∈ 𝑃)) → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
107	75, 88, 96, 104, 106	syl13anc 1375	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
108	44	recnd 11172	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℂ)
109	108, 17, 19, 21, 22, 25	divmuldivd 11970	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))))
110	53, 20	oveq12d 7386	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
111	109, 110	eqtrd 2772	. . . . 5 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
112	111	oveq1d 7383	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
113		ttgcontlem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
114	101, 102	grpsubcl 18962	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑋 − 𝐴) ∈ 𝑃)
115	98, 100, 113, 114	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ 𝑃)
116		ttgcontlem1.y	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
117	116	oveq2d 7384	. . . . . . . . 9 ⊢ (𝜑 → ((1 − 𝐾) · (𝑋 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
118	19, 21	mulcomd 11165	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 · (1 − 𝐾)) = ((1 − 𝐾) · 𝐾))
119	118	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)))
120	101, 102	grpsubcl 18962	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑌 − 𝐴) ∈ 𝑃)
121	98, 99, 113, 120	syl3anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 − 𝐴) ∈ 𝑃)
122	101, 83, 105, 84	clmvsass 25057	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
123	75, 89, 94, 121, 122	syl13anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
124	101, 83, 105, 84	clmvsass 25057	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((1 − 𝐾) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
125	75, 94, 89, 121, 124	syl13anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
126	119, 123, 125	3eqtr3d 2780	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
127		eqid 2737	. . . . . . . . . . . . 13 ⊢ (-g‘(Scalar‘𝐻)) = (-g‘(Scalar‘𝐻))
128		clmlmod 25035	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ LMod)
129	75, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ LMod)
130	101, 105, 83, 84, 102, 127, 129, 92, 89, 121	lmodsubdir 20883	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
131	83, 84	clmsub 25048	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
132	75, 92, 89, 131	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 − 𝐾) = (1(-g‘(Scalar‘𝐻))𝐾))
133	132	oveq1d 7383	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)))
134	101, 105	clmvs1 25061	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑌 − 𝐴) ∈ 𝑃) → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
135	75, 121, 134	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
136	135	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 − 𝐴) = (1 · (𝑌 − 𝐴)))
137	136, 116	oveq12d 7386	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
138	130, 133, 137	3eqtr4d 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((𝑌 − 𝐴) − (𝑋 − 𝐴)))
139	101, 102	grpnnncan2 18979	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
140	98, 99, 100, 113, 139	syl13anc 1375	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
141	138, 140	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = (𝑌 − 𝑋))
142	141	oveq2d 7384	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = (𝐾 · (𝑌 − 𝑋)))
143	117, 126, 142	3eqtr2rd 2779	. . . . . . . 8 ⊢ (𝜑 → (𝐾 · (𝑌 − 𝑋)) = ((1 − 𝐾) · (𝑋 − 𝐴)))
144	101, 105, 83, 84, 74, 89, 94, 104, 115, 57, 143	cvsmuleqdivd 25102	. . . . . . 7 ⊢ (𝜑 → (𝑌 − 𝑋) = (((1 − 𝐾) / 𝐾) · (𝑋 − 𝐴)))
145	101, 105, 83, 84, 74, 94, 89, 104, 115, 25, 57, 144	cvsdiveqd 25103	. . . . . 6 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = (𝑋 − 𝐴))
146	145, 115	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) ∈ 𝑃)
147		ttgcontlem1.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))
148		ttgcontlem1.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ 𝑃)
149	101, 102	grpsubcl 18962	. . . . . . . . . 10 ⊢ ((𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑁 − 𝐴) ∈ 𝑃)
150	98, 148, 113, 149	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − 𝐴) ∈ 𝑃)
151	101, 83, 105, 84	lmodvscl 20841	. . . . . . . . 9 ⊢ ((𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃) → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
152	129, 77, 150, 151	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
153		ttgitvval.p	. . . . . . . . 9 ⊢ + = (+g‘𝐻)
154	101, 153	grpcl 18883	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
155	98, 113, 152, 154	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
156	147, 155	eqeltrd 2837	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
157	101, 102	grpsubcl 18962	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝐵 − 𝑋) ∈ 𝑃)
158	98, 156, 100, 157	syl3anc 1374	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ 𝑃)
159		ttgcontlem1.r	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 𝑀)
160	52, 17, 159	subne0d 11513	. . . . 5 ⊢ (𝜑 → (𝐿 − 𝑀) ≠ 0)
161		ttgcontlem1.x	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
162	161	oveq2d 7384	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑋 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
163	17, 108	mulcomd 11165	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · (𝐿 − 𝑀)) = ((𝐿 − 𝑀) · 𝑀))
164	163	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)))
165	101, 83, 105, 84	clmvsass 25057	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑀 ∈ 𝑅 ∧ (𝐿 − 𝑀) ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
166	75, 82, 86, 150, 165	syl13anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
167	101, 83, 105, 84	clmvsass 25057	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
168	75, 86, 82, 150, 167	syl13anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
169	164, 166, 168	3eqtr3d 2780	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
170	101, 105, 83, 84, 102, 127, 129, 77, 82, 150	lmodsubdir 20883	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
171	83, 84	clmsub 25048	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
172	75, 77, 82, 171	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀))
173	172	oveq1d 7383	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)))
174	147	oveq1d 7383	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴))
175		lmodabl 20872	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ LMod → 𝐻 ∈ Abel)
176	129, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ Abel)
177	101, 153, 102	ablpncan2 19756	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
178	176, 113, 152, 177	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
179	174, 178	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
180	179, 161	oveq12d 7386	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
181	170, 173, 180	3eqtr4d 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐵 − 𝐴) − (𝑋 − 𝐴)))
182	101, 102	grpnnncan2 18979	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
183	98, 156, 100, 113, 182	syl13anc 1375	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
184	181, 183	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = (𝐵 − 𝑋))
185	184	oveq2d 7384	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = (𝑀 · (𝐵 − 𝑋)))
186	162, 169, 185	3eqtr2rd 2779	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (𝐵 − 𝑋)) = ((𝐿 − 𝑀) · (𝑋 − 𝐴)))
187	101, 105, 83, 84, 74, 82, 86, 158, 115, 22, 186	cvsmuleqdivd 25102	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑋) = (((𝐿 − 𝑀) / 𝑀) · (𝑋 − 𝐴)))
188	101, 105, 83, 84, 74, 86, 82, 158, 115, 160, 22, 187	cvsdiveqd 25103	. . . . . 6 ⊢ (𝜑 → ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)) = (𝑋 − 𝐴))
189	145, 188	eqtr4d 2775	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)))
190	101, 105, 83, 84, 74, 82, 86, 146, 158, 22, 160, 189	cvsdiveqd 25103	. . . 4 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))) = (𝐵 − 𝑋))
191	107, 112, 190	3eqtr3rd 2781	. . 3 ⊢ (𝜑 → (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
192		oveq1 7375	. . . 4 ⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → (𝑘 · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
193	192	rspceeqv 3601	. . 3 ⊢ (((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ∧ (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))
194	73, 191, 193	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))
195		ttgval.n	. . 3 ⊢ 𝐺 = (toTG‘𝐻)
196		ttgitvval.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
197	195, 196, 101, 102, 105, 100, 99, 74, 156	ttgelitv 28967	. 2 ⊢ (𝜑 → (𝐵 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
198	194, 197	mpbird 257	1 ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∃wrex 3062   ⊆ wss 3903   class class class wbr 5100  ‘cfv 6500  (class class class)co 7368  ℝcr 11037  0cc0 11038  1c1 11039   · cmul 11043  ℝ^*cxr 11177   < clt 11178   ≤ cle 11179   − cmin 11376   / cdiv 11806  ℝ⁺crp 12917  [,]cicc 13276  Basecbs 17148  +_gcplusg 17189  Scalarcsca 17192   ·_𝑠 cvsca 17193  Grpcgrp 18875  -_gcsg 18877  Abelcabl 19722  LModclmod 20823  ℂModcclm 25030  ℂVecccvs 25091  Itvcitv 28517  toTGcttg 28957

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 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-addf 11117  ax-mulf 11118

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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-z 12501  df-dec 12620  df-uz 12764  df-rp 12918  df-icc 13280  df-fz 13436  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-tset 17208  df-ple 17209  df-ds 17211  df-unif 17212  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878  df-minusg 18879  df-sbg 18880  df-subg 19065  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-ring 20182  df-cring 20183  df-oppr 20285  df-dvdsr 20305  df-unit 20306  df-invr 20336  df-dvr 20349  df-subrg 20515  df-drng 20676  df-lmod 20825  df-lvec 21067  df-cnfld 21322  df-clm 25031  df-cvs 25092  df-itv 28519  df-lng 28520  df-ttg 28958

This theorem is referenced by: (None)