Theorem ttgcontlem1 25765

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

Hypotheses

Ref	Expression
ttgval.n	|- G = (toTG ` H )
ttgitvval.i	|- I = (Itv ` G )
ttgitvval.b	|- P = ( Base ` H )
ttgitvval.m	|- .- = ( -g ` H )
ttgitvval.s	|- .x. = ( .s ` H )
ttgelitv.x	|- ( ph -> X e. P )
ttgelitv.y	|- ( ph -> Y e. P )
ttgbtwnid.r	|- R = ( Base ` (Scalar ` H ) )
ttgbtwnid.2	|- ( ph -> ( 0 [,] 1 ) C_ R )
ttgitvval.p	|- .+ = ( +g ` H )
ttgcontlem1.h	|- ( ph -> H e. CVec )
ttgcontlem1.a	|- ( ph -> A e. P )
ttgcontlem1.n	|- ( ph -> N e. P )
ttgcontlem1.o	|- ( ph -> M =/= 0 )
ttgcontlem1.p	|- ( ph -> K =/= 0 )
ttgcontlem1.q	|- ( ph -> K =/= 1 )
ttgcontlem1.r	|- ( ph -> L =/= M )
ttgcontlem1.s	|- ( ph -> L <_ ( M / K ) )
ttgcontlem1.l	|- ( ph -> L e. ( 0 [,] 1 ) )
ttgcontlem1.k	|- ( ph -> K e. ( 0 [,] 1 ) )
ttgcontlem1.m	|- ( ph -> M e. ( 0 [,] L ) )
ttgcontlem1.y	|- ( ph -> ( X .- A ) = ( K .x. ( Y .- A ) ) )
ttgcontlem1.x	|- ( ph -> ( X .- A ) = ( M .x. ( N .- A ) ) )
ttgcontlem1.b	|- ( ph -> B = ( A .+ ( L .x. ( N .- A ) ) ) )

Assertion

Ref	Expression
ttgcontlem1	|- ( ph -> B e. ( X I Y ) )

Proof of Theorem ttgcontlem1

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unitssre 12319	. . . . . . . 8 |- ( 0 [,] 1 ) C_ RR
2		ttgcontlem1.l	. . . . . . . 8 |- ( ph -> L e. ( 0 [,] 1 ) )
3	1, 2	sseldi 3601	. . . . . . 7 |- ( ph -> L e. RR )
4		ttgcontlem1.k	. . . . . . . 8 |- ( ph -> K e. ( 0 [,] 1 ) )
5	1, 4	sseldi 3601	. . . . . . 7 |- ( ph -> K e. RR )
6	3, 5	remulcld 10070	. . . . . 6 |- ( ph -> ( L x. K ) e. RR )
7		0re 10040	. . . . . . . . 9 |- 0 e. RR
8		iccssre 12255	. . . . . . . . 9 |- ( ( 0 e. RR /\ L e. RR ) -> ( 0 [,] L ) C_ RR )
9	7, 3, 8	sylancr 695	. . . . . . . 8 |- ( ph -> ( 0 [,] L ) C_ RR )
10		ttgcontlem1.m	. . . . . . . 8 |- ( ph -> M e. ( 0 [,] L ) )
11	9, 10	sseldd 3604	. . . . . . 7 |- ( ph -> M e. RR )
12	11, 5	remulcld 10070	. . . . . 6 |- ( ph -> ( M x. K ) e. RR )
13	6, 12	resubcld 10458	. . . . 5 |- ( ph -> ( ( L x. K ) - ( M x. K ) ) e. RR )
14		1red 10055	. . . . . . 7 |- ( ph -> 1 e. RR )
15	11, 14	remulcld 10070	. . . . . 6 |- ( ph -> ( M x. 1 ) e. RR )
16	15, 12	resubcld 10458	. . . . 5 |- ( ph -> ( ( M x. 1 ) - ( M x. K ) ) e. RR )
17	11	recnd 10068	. . . . . . 7 |- ( ph -> M e. CC )
18		1cnd 10056	. . . . . . 7 |- ( ph -> 1 e. CC )
19	5	recnd 10068	. . . . . . 7 |- ( ph -> K e. CC )
20	17, 18, 19	subdid 10486	. . . . . 6 |- ( ph -> ( M x. ( 1 - K ) ) = ( ( M x. 1 ) - ( M x. K ) ) )
21	18, 19	subcld 10392	. . . . . . 7 |- ( ph -> ( 1 - K ) e. CC )
22		ttgcontlem1.o	. . . . . . 7 |- ( ph -> M =/= 0 )
23		ttgcontlem1.q	. . . . . . . . 9 |- ( ph -> K =/= 1 )
24	23	necomd 2849	. . . . . . . 8 |- ( ph -> 1 =/= K )
25	18, 19, 24	subne0d 10401	. . . . . . 7 |- ( ph -> ( 1 - K ) =/= 0 )
26	17, 21, 22, 25	mulne0d 10679	. . . . . 6 |- ( ph -> ( M x. ( 1 - K ) ) =/= 0 )
27	20, 26	eqnetrrd 2862	. . . . 5 |- ( ph -> ( ( M x. 1 ) - ( M x. K ) ) =/= 0 )
28	13, 16, 27	redivcld 10853	. . . 4 |- ( ph -> ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. RR )
29		0xr 10086	. . . . . . . . . . 11 |- 0 e. RR*
30	29	a1i 11	. . . . . . . . . 10 |- ( ph -> 0 e. RR* )
31	3	rexrd 10089	. . . . . . . . . 10 |- ( ph -> L e. RR* )
32		iccgelb 12230	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ L e. RR* /\ M e. ( 0 [,] L ) ) -> 0 <_ M )
33	30, 31, 10, 32	syl3anc 1326	. . . . . . . . 9 |- ( ph -> 0 <_ M )
34	11, 33, 22	ne0gt0d 10174	. . . . . . . 8 |- ( ph -> 0 < M )
35	11, 34	elrpd 11869	. . . . . . 7 |- ( ph -> M e. RR+ )
36	14	rexrd 10089	. . . . . . . . . 10 |- ( ph -> 1 e. RR* )
37		iccleub 12229	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ 1 e. RR* /\ K e. ( 0 [,] 1 ) ) -> K <_ 1 )
38	30, 36, 4, 37	syl3anc 1326	. . . . . . . . 9 |- ( ph -> K <_ 1 )
39	5, 14	ltlend 10182	. . . . . . . . 9 |- ( ph -> ( K < 1 <-> ( K <_ 1 /\ 1 =/= K ) ) )
40	38, 24, 39	mpbir2and 957	. . . . . . . 8 |- ( ph -> K < 1 )
41		difrp 11868	. . . . . . . . 9 |- ( ( K e. RR /\ 1 e. RR ) -> ( K < 1 <-> ( 1 - K ) e. RR+ ) )
42	5, 14, 41	syl2anc 693	. . . . . . . 8 |- ( ph -> ( K < 1 <-> ( 1 - K ) e. RR+ ) )
43	40, 42	mpbid 222	. . . . . . 7 |- ( ph -> ( 1 - K ) e. RR+ )
44	35, 43	rpmulcld 11888	. . . . . 6 |- ( ph -> ( M x. ( 1 - K ) ) e. RR+ )
45	20, 44	eqeltrrd 2702	. . . . 5 |- ( ph -> ( ( M x. 1 ) - ( M x. K ) ) e. RR+ )
46	3, 11	resubcld 10458	. . . . . . 7 |- ( ph -> ( L - M ) e. RR )
47		iccleub 12229	. . . . . . . . 9 |- ( ( 0 e. RR* /\ L e. RR* /\ M e. ( 0 [,] L ) ) -> M <_ L )
48	30, 31, 10, 47	syl3anc 1326	. . . . . . . 8 |- ( ph -> M <_ L )
49	3, 11	subge0d 10617	. . . . . . . 8 |- ( ph -> ( 0 <_ ( L - M ) <-> M <_ L ) )
50	48, 49	mpbird 247	. . . . . . 7 |- ( ph -> 0 <_ ( L - M ) )
51		iccgelb 12230	. . . . . . . 8 |- ( ( 0 e. RR* /\ 1 e. RR* /\ K e. ( 0 [,] 1 ) ) -> 0 <_ K )
52	30, 36, 4, 51	syl3anc 1326	. . . . . . 7 |- ( ph -> 0 <_ K )
53	46, 5, 50, 52	mulge0d 10604	. . . . . 6 |- ( ph -> 0 <_ ( ( L - M ) x. K ) )
54	3	recnd 10068	. . . . . . 7 |- ( ph -> L e. CC )
55	54, 17, 19	subdird 10487	. . . . . 6 |- ( ph -> ( ( L - M ) x. K ) = ( ( L x. K ) - ( M x. K ) ) )
56	53, 55	breqtrd 4679	. . . . 5 |- ( ph -> 0 <_ ( ( L x. K ) - ( M x. K ) ) )
57	13, 45, 56	divge0d 11912	. . . 4 |- ( ph -> 0 <_ ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) )
58		ttgcontlem1.s	. . . . . . . . 9 |- ( ph -> L <_ ( M / K ) )
59		ttgcontlem1.p	. . . . . . . . . . . 12 |- ( ph -> K =/= 0 )
60	5, 52, 59	ne0gt0d 10174	. . . . . . . . . . 11 |- ( ph -> 0 < K )
61	5, 60	elrpd 11869	. . . . . . . . . 10 |- ( ph -> K e. RR+ )
62	3, 11, 61	lemuldivd 11921	. . . . . . . . 9 |- ( ph -> ( ( L x. K ) <_ M <-> L <_ ( M / K ) ) )
63	58, 62	mpbird 247	. . . . . . . 8 |- ( ph -> ( L x. K ) <_ M )
64	17	mulid1d 10057	. . . . . . . 8 |- ( ph -> ( M x. 1 ) = M )
65	63, 64	breqtrrd 4681	. . . . . . 7 |- ( ph -> ( L x. K ) <_ ( M x. 1 ) )
66	6, 15, 12, 65	lesub1dd 10643	. . . . . 6 |- ( ph -> ( ( L x. K ) - ( M x. K ) ) <_ ( ( M x. 1 ) - ( M x. K ) ) )
67	17, 18	mulcld 10060	. . . . . . . 8 |- ( ph -> ( M x. 1 ) e. CC )
68	17, 19	mulcld 10060	. . . . . . . 8 |- ( ph -> ( M x. K ) e. CC )
69	67, 68	subcld 10392	. . . . . . 7 |- ( ph -> ( ( M x. 1 ) - ( M x. K ) ) e. CC )
70	69	mulid1d 10057	. . . . . 6 |- ( ph -> ( ( ( M x. 1 ) - ( M x. K ) ) x. 1 ) = ( ( M x. 1 ) - ( M x. K ) ) )
71	66, 70	breqtrrd 4681	. . . . 5 |- ( ph -> ( ( L x. K ) - ( M x. K ) ) <_ ( ( ( M x. 1 ) - ( M x. K ) ) x. 1 ) )
72	13, 14, 45	ledivmuld 11925	. . . . 5 |- ( ph -> ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) <_ 1 <-> ( ( L x. K ) - ( M x. K ) ) <_ ( ( ( M x. 1 ) - ( M x. K ) ) x. 1 ) ) )
73	71, 72	mpbird 247	. . . 4 |- ( ph -> ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) <_ 1 )
74		1re 10039	. . . . 5 |- 1 e. RR
75	7, 74	elicc2i 12239	. . . 4 |- ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. ( 0 [,] 1 ) <-> ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. RR /\ 0 <_ ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) /\ ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) <_ 1 ) )
76	28, 57, 73, 75	syl3anbrc 1246	. . 3 |- ( ph -> ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. ( 0 [,] 1 ) )
77		ttgcontlem1.h	. . . . . 6 |- ( ph -> H e. CVec )
78	77	cvsclm 22926	. . . . 5 |- ( ph -> H e. CMod )
79		ttgbtwnid.2	. . . . . . . 8 |- ( ph -> ( 0 [,] 1 ) C_ R )
80	79, 2	sseldd 3604	. . . . . . 7 |- ( ph -> L e. R )
81		0elunit 12290	. . . . . . . . . 10 |- 0 e. ( 0 [,] 1 )
82		iccss2 12244	. . . . . . . . . 10 |- ( ( 0 e. ( 0 [,] 1 ) /\ L e. ( 0 [,] 1 ) ) -> ( 0 [,] L ) C_ ( 0 [,] 1 ) )
83	81, 2, 82	sylancr 695	. . . . . . . . 9 |- ( ph -> ( 0 [,] L ) C_ ( 0 [,] 1 ) )
84	83, 79	sstrd 3613	. . . . . . . 8 |- ( ph -> ( 0 [,] L ) C_ R )
85	84, 10	sseldd 3604	. . . . . . 7 |- ( ph -> M e. R )
86		eqid 2622	. . . . . . . 8 |- (Scalar ` H ) = (Scalar ` H )
87		ttgbtwnid.r	. . . . . . . 8 |- R = ( Base ` (Scalar ` H ) )
88	86, 87	clmsubcl 22886	. . . . . . 7 |- ( ( H e. CMod /\ L e. R /\ M e. R ) -> ( L - M ) e. R )
89	78, 80, 85, 88	syl3anc 1326	. . . . . 6 |- ( ph -> ( L - M ) e. R )
90	86, 87	cvsdivcl 22933	. . . . . 6 |- ( ( H e. CVec /\ ( ( L - M ) e. R /\ M e. R /\ M =/= 0 ) ) -> ( ( L - M ) / M ) e. R )
91	77, 89, 85, 22, 90	syl13anc 1328	. . . . 5 |- ( ph -> ( ( L - M ) / M ) e. R )
92	79, 4	sseldd 3604	. . . . . 6 |- ( ph -> K e. R )
93		1elunit 12291	. . . . . . . . 9 |- 1 e. ( 0 [,] 1 )
94	93	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. ( 0 [,] 1 ) )
95	79, 94	sseldd 3604	. . . . . . 7 |- ( ph -> 1 e. R )
96	86, 87	clmsubcl 22886	. . . . . . 7 |- ( ( H e. CMod /\ 1 e. R /\ K e. R ) -> ( 1 - K ) e. R )
97	78, 95, 92, 96	syl3anc 1326	. . . . . 6 |- ( ph -> ( 1 - K ) e. R )
98	86, 87	cvsdivcl 22933	. . . . . 6 |- ( ( H e. CVec /\ ( K e. R /\ ( 1 - K ) e. R /\ ( 1 - K ) =/= 0 ) ) -> ( K / ( 1 - K ) ) e. R )
99	77, 92, 97, 25, 98	syl13anc 1328	. . . . 5 |- ( ph -> ( K / ( 1 - K ) ) e. R )
100		clmgrp 22868	. . . . . . 7 |- ( H e. CMod -> H e. Grp )
101	78, 100	syl 17	. . . . . 6 |- ( ph -> H e. Grp )
102		ttgelitv.y	. . . . . 6 |- ( ph -> Y e. P )
103		ttgelitv.x	. . . . . 6 |- ( ph -> X e. P )
104		ttgitvval.b	. . . . . . 7 |- P = ( Base ` H )
105		ttgitvval.m	. . . . . . 7 |- .- = ( -g ` H )
106	104, 105	grpsubcl 17495	. . . . . 6 |- ( ( H e. Grp /\ Y e. P /\ X e. P ) -> ( Y .- X ) e. P )
107	101, 102, 103, 106	syl3anc 1326	. . . . 5 |- ( ph -> ( Y .- X ) e. P )
108		ttgitvval.s	. . . . . 6 |- .x. = ( .s ` H )
109	104, 86, 108, 87	clmvsass 22889	. . . . 5 |- ( ( H e. CMod /\ ( ( ( L - M ) / M ) e. R /\ ( K / ( 1 - K ) ) e. R /\ ( Y .- X ) e. P ) ) -> ( ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) .x. ( Y .- X ) ) = ( ( ( L - M ) / M ) .x. ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) ) )
110	78, 91, 99, 107, 109	syl13anc 1328	. . . 4 |- ( ph -> ( ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) .x. ( Y .- X ) ) = ( ( ( L - M ) / M ) .x. ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) ) )
111	46	recnd 10068	. . . . . . 7 |- ( ph -> ( L - M ) e. CC )
112	111, 17, 19, 21, 22, 25	divmuldivd 10842	. . . . . 6 |- ( ph -> ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) = ( ( ( L - M ) x. K ) / ( M x. ( 1 - K ) ) ) )
113	55, 20	oveq12d 6668	. . . . . 6 |- ( ph -> ( ( ( L - M ) x. K ) / ( M x. ( 1 - K ) ) ) = ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) )
114	112, 113	eqtrd 2656	. . . . 5 |- ( ph -> ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) = ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) )
115	114	oveq1d 6665	. . . 4 |- ( ph -> ( ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) .x. ( Y .- X ) ) = ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) .x. ( Y .- X ) ) )
116		ttgcontlem1.a	. . . . . . . 8 |- ( ph -> A e. P )
117	104, 105	grpsubcl 17495	. . . . . . . 8 |- ( ( H e. Grp /\ X e. P /\ A e. P ) -> ( X .- A ) e. P )
118	101, 103, 116, 117	syl3anc 1326	. . . . . . 7 |- ( ph -> ( X .- A ) e. P )
119		ttgcontlem1.y	. . . . . . . . . 10 |- ( ph -> ( X .- A ) = ( K .x. ( Y .- A ) ) )
120	119	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( ( 1 - K ) .x. ( X .- A ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
121	19, 21	mulcomd 10061	. . . . . . . . . . 11 |- ( ph -> ( K x. ( 1 - K ) ) = ( ( 1 - K ) x. K ) )
122	121	oveq1d 6665	. . . . . . . . . 10 |- ( ph -> ( ( K x. ( 1 - K ) ) .x. ( Y .- A ) ) = ( ( ( 1 - K ) x. K ) .x. ( Y .- A ) ) )
123	104, 105	grpsubcl 17495	. . . . . . . . . . . 12 |- ( ( H e. Grp /\ Y e. P /\ A e. P ) -> ( Y .- A ) e. P )
124	101, 102, 116, 123	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( Y .- A ) e. P )
125	104, 86, 108, 87	clmvsass 22889	. . . . . . . . . . 11 |- ( ( H e. CMod /\ ( K e. R /\ ( 1 - K ) e. R /\ ( Y .- A ) e. P ) ) -> ( ( K x. ( 1 - K ) ) .x. ( Y .- A ) ) = ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) )
126	78, 92, 97, 124, 125	syl13anc 1328	. . . . . . . . . 10 |- ( ph -> ( ( K x. ( 1 - K ) ) .x. ( Y .- A ) ) = ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) )
127	104, 86, 108, 87	clmvsass 22889	. . . . . . . . . . 11 |- ( ( H e. CMod /\ ( ( 1 - K ) e. R /\ K e. R /\ ( Y .- A ) e. P ) ) -> ( ( ( 1 - K ) x. K ) .x. ( Y .- A ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
128	78, 97, 92, 124, 127	syl13anc 1328	. . . . . . . . . 10 |- ( ph -> ( ( ( 1 - K ) x. K ) .x. ( Y .- A ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
129	122, 126, 128	3eqtr3d 2664	. . . . . . . . 9 |- ( ph -> ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
130		eqid 2622	. . . . . . . . . . . . 13 |- ( -g ` (Scalar ` H ) ) = ( -g ` (Scalar ` H ) )
131		clmlmod 22867	. . . . . . . . . . . . . 14 |- ( H e. CMod -> H e. LMod )
132	78, 131	syl 17	. . . . . . . . . . . . 13 |- ( ph -> H e. LMod )
133	104, 108, 86, 87, 105, 130, 132, 95, 92, 124	lmodsubdir 18921	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 ( -g ` (Scalar ` H ) ) K ) .x. ( Y .- A ) ) = ( ( 1 .x. ( Y .- A ) ) .- ( K .x. ( Y .- A ) ) ) )
134	86, 87	clmsub 22880	. . . . . . . . . . . . . 14 |- ( ( H e. CMod /\ 1 e. R /\ K e. R ) -> ( 1 - K ) = ( 1 ( -g ` (Scalar ` H ) ) K ) )
135	78, 95, 92, 134	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ph -> ( 1 - K ) = ( 1 ( -g ` (Scalar ` H ) ) K ) )
136	135	oveq1d 6665	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 - K ) .x. ( Y .- A ) ) = ( ( 1 ( -g ` (Scalar ` H ) ) K ) .x. ( Y .- A ) ) )
137	104, 108	clmvs1 22893	. . . . . . . . . . . . . . 15 |- ( ( H e. CMod /\ ( Y .- A ) e. P ) -> ( 1 .x. ( Y .- A ) ) = ( Y .- A ) )
138	78, 124, 137	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 .x. ( Y .- A ) ) = ( Y .- A ) )
139	138	eqcomd 2628	. . . . . . . . . . . . 13 |- ( ph -> ( Y .- A ) = ( 1 .x. ( Y .- A ) ) )
140	139, 119	oveq12d 6668	. . . . . . . . . . . 12 |- ( ph -> ( ( Y .- A ) .- ( X .- A ) ) = ( ( 1 .x. ( Y .- A ) ) .- ( K .x. ( Y .- A ) ) ) )
141	133, 136, 140	3eqtr4d 2666	. . . . . . . . . . 11 |- ( ph -> ( ( 1 - K ) .x. ( Y .- A ) ) = ( ( Y .- A ) .- ( X .- A ) ) )
142	104, 105	grpnnncan2 17512	. . . . . . . . . . . 12 |- ( ( H e. Grp /\ ( Y e. P /\ X e. P /\ A e. P ) ) -> ( ( Y .- A ) .- ( X .- A ) ) = ( Y .- X ) )
143	101, 102, 103, 116, 142	syl13anc 1328	. . . . . . . . . . 11 |- ( ph -> ( ( Y .- A ) .- ( X .- A ) ) = ( Y .- X ) )
144	141, 143	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( ( 1 - K ) .x. ( Y .- A ) ) = ( Y .- X ) )
145	144	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) = ( K .x. ( Y .- X ) ) )
146	120, 129, 145	3eqtr2rd 2663	. . . . . . . 8 |- ( ph -> ( K .x. ( Y .- X ) ) = ( ( 1 - K ) .x. ( X .- A ) ) )
147	104, 108, 86, 87, 77, 92, 97, 107, 118, 59, 146	cvsmuleqdivd 22934	. . . . . . 7 |- ( ph -> ( Y .- X ) = ( ( ( 1 - K ) / K ) .x. ( X .- A ) ) )
148	104, 108, 86, 87, 77, 97, 92, 107, 118, 25, 59, 147	cvsdiveqd 22935	. . . . . 6 |- ( ph -> ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) = ( X .- A ) )
149	148, 118	eqeltrd 2701	. . . . 5 |- ( ph -> ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) e. P )
150		ttgcontlem1.b	. . . . . . 7 |- ( ph -> B = ( A .+ ( L .x. ( N .- A ) ) ) )
151		ttgcontlem1.n	. . . . . . . . . 10 |- ( ph -> N e. P )
152	104, 105	grpsubcl 17495	. . . . . . . . . 10 |- ( ( H e. Grp /\ N e. P /\ A e. P ) -> ( N .- A ) e. P )
153	101, 151, 116, 152	syl3anc 1326	. . . . . . . . 9 |- ( ph -> ( N .- A ) e. P )
154	104, 86, 108, 87	lmodvscl 18880	. . . . . . . . 9 |- ( ( H e. LMod /\ L e. R /\ ( N .- A ) e. P ) -> ( L .x. ( N .- A ) ) e. P )
155	132, 80, 153, 154	syl3anc 1326	. . . . . . . 8 |- ( ph -> ( L .x. ( N .- A ) ) e. P )
156		ttgitvval.p	. . . . . . . . 9 |- .+ = ( +g ` H )
157	104, 156	grpcl 17430	. . . . . . . 8 |- ( ( H e. Grp /\ A e. P /\ ( L .x. ( N .- A ) ) e. P ) -> ( A .+ ( L .x. ( N .- A ) ) ) e. P )
158	101, 116, 155, 157	syl3anc 1326	. . . . . . 7 |- ( ph -> ( A .+ ( L .x. ( N .- A ) ) ) e. P )
159	150, 158	eqeltrd 2701	. . . . . 6 |- ( ph -> B e. P )
160	104, 105	grpsubcl 17495	. . . . . 6 |- ( ( H e. Grp /\ B e. P /\ X e. P ) -> ( B .- X ) e. P )
161	101, 159, 103, 160	syl3anc 1326	. . . . 5 |- ( ph -> ( B .- X ) e. P )
162		ttgcontlem1.r	. . . . . 6 |- ( ph -> L =/= M )
163	54, 17, 162	subne0d 10401	. . . . 5 |- ( ph -> ( L - M ) =/= 0 )
164		ttgcontlem1.x	. . . . . . . . . 10 |- ( ph -> ( X .- A ) = ( M .x. ( N .- A ) ) )
165	164	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( ( L - M ) .x. ( X .- A ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
166	17, 111	mulcomd 10061	. . . . . . . . . . 11 |- ( ph -> ( M x. ( L - M ) ) = ( ( L - M ) x. M ) )
167	166	oveq1d 6665	. . . . . . . . . 10 |- ( ph -> ( ( M x. ( L - M ) ) .x. ( N .- A ) ) = ( ( ( L - M ) x. M ) .x. ( N .- A ) ) )
168	104, 86, 108, 87	clmvsass 22889	. . . . . . . . . . 11 |- ( ( H e. CMod /\ ( M e. R /\ ( L - M ) e. R /\ ( N .- A ) e. P ) ) -> ( ( M x. ( L - M ) ) .x. ( N .- A ) ) = ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) )
169	78, 85, 89, 153, 168	syl13anc 1328	. . . . . . . . . 10 |- ( ph -> ( ( M x. ( L - M ) ) .x. ( N .- A ) ) = ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) )
170	104, 86, 108, 87	clmvsass 22889	. . . . . . . . . . 11 |- ( ( H e. CMod /\ ( ( L - M ) e. R /\ M e. R /\ ( N .- A ) e. P ) ) -> ( ( ( L - M ) x. M ) .x. ( N .- A ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
171	78, 89, 85, 153, 170	syl13anc 1328	. . . . . . . . . 10 |- ( ph -> ( ( ( L - M ) x. M ) .x. ( N .- A ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
172	167, 169, 171	3eqtr3d 2664	. . . . . . . . 9 |- ( ph -> ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
173	104, 108, 86, 87, 105, 130, 132, 80, 85, 153	lmodsubdir 18921	. . . . . . . . . . . 12 |- ( ph -> ( ( L ( -g ` (Scalar ` H ) ) M ) .x. ( N .- A ) ) = ( ( L .x. ( N .- A ) ) .- ( M .x. ( N .- A ) ) ) )
174	86, 87	clmsub 22880	. . . . . . . . . . . . . 14 |- ( ( H e. CMod /\ L e. R /\ M e. R ) -> ( L - M ) = ( L ( -g ` (Scalar ` H ) ) M ) )
175	78, 80, 85, 174	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ph -> ( L - M ) = ( L ( -g ` (Scalar ` H ) ) M ) )
176	175	oveq1d 6665	. . . . . . . . . . . 12 |- ( ph -> ( ( L - M ) .x. ( N .- A ) ) = ( ( L ( -g ` (Scalar ` H ) ) M ) .x. ( N .- A ) ) )
177	150	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ph -> ( B .- A ) = ( ( A .+ ( L .x. ( N .- A ) ) ) .- A ) )
178		lmodabl 18910	. . . . . . . . . . . . . . . 16 |- ( H e. LMod -> H e. Abel )
179	132, 178	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> H e. Abel )
180	104, 156, 105	ablpncan2 18221	. . . . . . . . . . . . . . 15 |- ( ( H e. Abel /\ A e. P /\ ( L .x. ( N .- A ) ) e. P ) -> ( ( A .+ ( L .x. ( N .- A ) ) ) .- A ) = ( L .x. ( N .- A ) ) )
181	179, 116, 155, 180	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ph -> ( ( A .+ ( L .x. ( N .- A ) ) ) .- A ) = ( L .x. ( N .- A ) ) )
182	177, 181	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ph -> ( B .- A ) = ( L .x. ( N .- A ) ) )
183	182, 164	oveq12d 6668	. . . . . . . . . . . 12 |- ( ph -> ( ( B .- A ) .- ( X .- A ) ) = ( ( L .x. ( N .- A ) ) .- ( M .x. ( N .- A ) ) ) )
184	173, 176, 183	3eqtr4d 2666	. . . . . . . . . . 11 |- ( ph -> ( ( L - M ) .x. ( N .- A ) ) = ( ( B .- A ) .- ( X .- A ) ) )
185	104, 105	grpnnncan2 17512	. . . . . . . . . . . 12 |- ( ( H e. Grp /\ ( B e. P /\ X e. P /\ A e. P ) ) -> ( ( B .- A ) .- ( X .- A ) ) = ( B .- X ) )
186	101, 159, 103, 116, 185	syl13anc 1328	. . . . . . . . . . 11 |- ( ph -> ( ( B .- A ) .- ( X .- A ) ) = ( B .- X ) )
187	184, 186	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( ( L - M ) .x. ( N .- A ) ) = ( B .- X ) )
188	187	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) = ( M .x. ( B .- X ) ) )
189	165, 172, 188	3eqtr2rd 2663	. . . . . . . 8 |- ( ph -> ( M .x. ( B .- X ) ) = ( ( L - M ) .x. ( X .- A ) ) )
190	104, 108, 86, 87, 77, 85, 89, 161, 118, 22, 189	cvsmuleqdivd 22934	. . . . . . 7 |- ( ph -> ( B .- X ) = ( ( ( L - M ) / M ) .x. ( X .- A ) ) )
191	104, 108, 86, 87, 77, 89, 85, 161, 118, 163, 22, 190	cvsdiveqd 22935	. . . . . 6 |- ( ph -> ( ( M / ( L - M ) ) .x. ( B .- X ) ) = ( X .- A ) )
192	148, 191	eqtr4d 2659	. . . . 5 |- ( ph -> ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) = ( ( M / ( L - M ) ) .x. ( B .- X ) ) )
193	104, 108, 86, 87, 77, 85, 89, 149, 161, 22, 163, 192	cvsdiveqd 22935	. . . 4 |- ( ph -> ( ( ( L - M ) / M ) .x. ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) ) = ( B .- X ) )
194	110, 115, 193	3eqtr3rd 2665	. . 3 |- ( ph -> ( B .- X ) = ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) .x. ( Y .- X ) ) )
195		oveq1 6657	. . . . 5 |- ( k = ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) -> ( k .x. ( Y .- X ) ) = ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) .x. ( Y .- X ) ) )
196	195	eqeq2d 2632	. . . 4 |- ( k = ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) -> ( ( B .- X ) = ( k .x. ( Y .- X ) ) <-> ( B .- X ) = ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) .x. ( Y .- X ) ) ) )
197	196	rspcev 3309	. . 3 |- ( ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. ( 0 [,] 1 ) /\ ( B .- X ) = ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) .x. ( Y .- X ) ) ) -> E. k e. ( 0 [,] 1 ) ( B .- X ) = ( k .x. ( Y .- X ) ) )
198	76, 194, 197	syl2anc 693	. 2 |- ( ph -> E. k e. ( 0 [,] 1 ) ( B .- X ) = ( k .x. ( Y .- X ) ) )
199		ttgval.n	. . 3 |- G = (toTG ` H )
200		ttgitvval.i	. . 3 |- I = (Itv ` G )
201	199, 200, 104, 105, 108, 103, 102, 77, 159	ttgelitv 25763	. 2 |- ( ph -> ( B e. ( X I Y ) <-> E. k e. ( 0 [,] 1 ) ( B .- X ) = ( k .x. ( Y .- X ) ) ) )
202	198, 201	mpbird 247	1 |- ( ph -> B e. ( X I Y ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   C_ wss 3574   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   RRcr 9935   0cc0 9936   1c1 9937   x. cmul 9941   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   RR+crp 11832   [,]cicc 12178   Basecbs 15857   +g cplusg 15941  Scalarcsca 15944   .scvsca 15945   Grpcgrp 17422   -gcsg 17424   Abelcabl 18194   LModclmod 18863  CModcclm 22862  CVecccvs 22923  Itvcitv 25335  toTGcttg 25753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-icc 12182  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-minusg 17426  df-sbg 17427  df-subg 17591  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-drng 18749  df-subrg 18778  df-lmod 18865  df-lvec 19103  df-cnfld 19747  df-clm 22863  df-cvs 22924  df-itv 25337  df-lng 25338  df-ttg 25754

This theorem is referenced by: (None)