Metamath Proof Explorer

Theorem ttgcontlem1

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

Ref Expression
Hypotheses 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 ttgcontlem1 
|- ( ph -> B e. ( X I Y ) )

Proof

Step Hyp Ref Expression
1 ttgval.n 
 |-  G = ( toTG ` H )
2 ttgitvval.i 
 |-  I = ( Itv ` G )
3 ttgitvval.b 
 |-  P = ( Base ` H )
4 ttgitvval.m 
 |-  .- = ( -g ` H )
5 ttgitvval.s 
 |-  .x. = ( .s ` H )
6 ttgelitv.x 
 |-  ( ph -> X e. P )
7 ttgelitv.y 
 |-  ( ph -> Y e. P )
8 ttgbtwnid.r 
 |-  R = ( Base ` ( Scalar ` H ) )
9 ttgbtwnid.2 
 |-  ( ph -> ( 0 [,] 1 ) C_ R )
10 ttgitvval.p 
 |-  .+ = ( +g ` H )
11 ttgcontlem1.h 
 |-  ( ph -> H e. CVec )
12 ttgcontlem1.a 
 |-  ( ph -> A e. P )
13 ttgcontlem1.n 
 |-  ( ph -> N e. P )
14 ttgcontlem1.o 
 |-  ( ph -> M =/= 0 )
15 ttgcontlem1.p 
 |-  ( ph -> K =/= 0 )
16 ttgcontlem1.q 
 |-  ( ph -> K =/= 1 )
17 ttgcontlem1.r 
 |-  ( ph -> L =/= M )
18 ttgcontlem1.s 
 |-  ( ph -> L <_ ( M / K ) )
19 ttgcontlem1.l 
 |-  ( ph -> L e. ( 0 [,] 1 ) )
20 ttgcontlem1.k 
 |-  ( ph -> K e. ( 0 [,] 1 ) )
21 ttgcontlem1.m 
 |-  ( ph -> M e. ( 0 [,] L ) )
22 ttgcontlem1.y 
 |-  ( ph -> ( X .- A ) = ( K .x. ( Y .- A ) ) )
23 ttgcontlem1.x 
 |-  ( ph -> ( X .- A ) = ( M .x. ( N .- A ) ) )
24 ttgcontlem1.b 
 |-  ( ph -> B = ( A .+ ( L .x. ( N .- A ) ) ) )
25 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
26 25 19 sseldi 
 |-  ( ph -> L e. RR )
27 25 20 sseldi 
 |-  ( ph -> K e. RR )
28 26 27 remulcld 
 |-  ( ph -> ( L x. K ) e. RR )
29 0re 
 |-  0 e. RR
30 iccssre 
 |-  ( ( 0 e. RR /\ L e. RR ) -> ( 0 [,] L ) C_ RR )
31 29 26 30 sylancr 
 |-  ( ph -> ( 0 [,] L ) C_ RR )
32 31 21 sseldd 
 |-  ( ph -> M e. RR )
33 32 27 remulcld 
 |-  ( ph -> ( M x. K ) e. RR )
34 28 33 resubcld 
 |-  ( ph -> ( ( L x. K ) - ( M x. K ) ) e. RR )
35 1red 
 |-  ( ph -> 1 e. RR )
36 32 35 remulcld 
 |-  ( ph -> ( M x. 1 ) e. RR )
37 36 33 resubcld 
 |-  ( ph -> ( ( M x. 1 ) - ( M x. K ) ) e. RR )
38 32 recnd 
 |-  ( ph -> M e. CC )
39 1cnd 
 |-  ( ph -> 1 e. CC )
40 27 recnd 
 |-  ( ph -> K e. CC )
41 38 39 40 subdid 
 |-  ( ph -> ( M x. ( 1 - K ) ) = ( ( M x. 1 ) - ( M x. K ) ) )
42 39 40 subcld 
 |-  ( ph -> ( 1 - K ) e. CC )
43 16 necomd 
 |-  ( ph -> 1 =/= K )
44 39 40 43 subne0d 
 |-  ( ph -> ( 1 - K ) =/= 0 )
45 38 42 14 44 mulne0d 
 |-  ( ph -> ( M x. ( 1 - K ) ) =/= 0 )
46 41 45 eqnetrrd 
 |-  ( ph -> ( ( M x. 1 ) - ( M x. K ) ) =/= 0 )
47 34 37 46 redivcld 
 |-  ( ph -> ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. RR )
48 0xr 
 |-  0 e. RR*
49 26 rexrd 
 |-  ( ph -> L e. RR* )
50 iccgelb 
 |-  ( ( 0 e. RR* /\ L e. RR* /\ M e. ( 0 [,] L ) ) -> 0 <_ M )
51 48 49 21 50 mp3an2i 
 |-  ( ph -> 0 <_ M )
52 32 51 14 ne0gt0d 
 |-  ( ph -> 0 < M )
53 32 52 elrpd 
 |-  ( ph -> M e. RR+ )
54 35 rexrd 
 |-  ( ph -> 1 e. RR* )
55 iccleub 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ K e. ( 0 [,] 1 ) ) -> K <_ 1 )
56 48 54 20 55 mp3an2i 
 |-  ( ph -> K <_ 1 )
57 27 35 56 43 leneltd 
 |-  ( ph -> K < 1 )
58 difrp 
 |-  ( ( K e. RR /\ 1 e. RR ) -> ( K < 1 <-> ( 1 - K ) e. RR+ ) )
59 27 35 58 syl2anc 
 |-  ( ph -> ( K < 1 <-> ( 1 - K ) e. RR+ ) )
60 57 59 mpbid 
 |-  ( ph -> ( 1 - K ) e. RR+ )
61 53 60 rpmulcld 
 |-  ( ph -> ( M x. ( 1 - K ) ) e. RR+ )
62 41 61 eqeltrrd 
 |-  ( ph -> ( ( M x. 1 ) - ( M x. K ) ) e. RR+ )
63 26 32 resubcld 
 |-  ( ph -> ( L - M ) e. RR )
64 iccleub 
 |-  ( ( 0 e. RR* /\ L e. RR* /\ M e. ( 0 [,] L ) ) -> M <_ L )
65 48 49 21 64 mp3an2i 
 |-  ( ph -> M <_ L )
66 26 32 subge0d 
 |-  ( ph -> ( 0 <_ ( L - M ) <-> M <_ L ) )
67 65 66 mpbird 
 |-  ( ph -> 0 <_ ( L - M ) )
68 iccgelb 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ K e. ( 0 [,] 1 ) ) -> 0 <_ K )
69 48 54 20 68 mp3an2i 
 |-  ( ph -> 0 <_ K )
70 63 27 67 69 mulge0d 
 |-  ( ph -> 0 <_ ( ( L - M ) x. K ) )
71 26 recnd 
 |-  ( ph -> L e. CC )
72 71 38 40 subdird 
 |-  ( ph -> ( ( L - M ) x. K ) = ( ( L x. K ) - ( M x. K ) ) )
73 70 72 breqtrd 
 |-  ( ph -> 0 <_ ( ( L x. K ) - ( M x. K ) ) )
74 34 62 73 divge0d 
 |-  ( ph -> 0 <_ ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) )
75 27 69 15 ne0gt0d 
 |-  ( ph -> 0 < K )
76 27 75 elrpd 
 |-  ( ph -> K e. RR+ )
77 26 32 76 lemuldivd 
 |-  ( ph -> ( ( L x. K ) <_ M <-> L <_ ( M / K ) ) )
78 18 77 mpbird 
 |-  ( ph -> ( L x. K ) <_ M )
79 38 mulid1d 
 |-  ( ph -> ( M x. 1 ) = M )
80 78 79 breqtrrd 
 |-  ( ph -> ( L x. K ) <_ ( M x. 1 ) )
81 28 36 33 80 lesub1dd 
 |-  ( ph -> ( ( L x. K ) - ( M x. K ) ) <_ ( ( M x. 1 ) - ( M x. K ) ) )
82 38 39 mulcld 
 |-  ( ph -> ( M x. 1 ) e. CC )
83 38 40 mulcld 
 |-  ( ph -> ( M x. K ) e. CC )
84 82 83 subcld 
 |-  ( ph -> ( ( M x. 1 ) - ( M x. K ) ) e. CC )
85 84 mulid1d 
 |-  ( ph -> ( ( ( M x. 1 ) - ( M x. K ) ) x. 1 ) = ( ( M x. 1 ) - ( M x. K ) ) )
86 81 85 breqtrrd 
 |-  ( ph -> ( ( L x. K ) - ( M x. K ) ) <_ ( ( ( M x. 1 ) - ( M x. K ) ) x. 1 ) )
87 34 35 62 ledivmuld 
 |-  ( 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 ) ) )
88 86 87 mpbird 
 |-  ( ph -> ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) <_ 1 )
89 elicc01 
 |-  ( ( ( ( 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 ) )
90 47 74 88 89 syl3anbrc 
 |-  ( ph -> ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) e. ( 0 [,] 1 ) )
91 11 cvsclm 
 |-  ( ph -> H e. CMod )
92 9 19 sseldd 
 |-  ( ph -> L e. R )
93 0elunit 
 |-  0 e. ( 0 [,] 1 )
94 iccss2 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ L e. ( 0 [,] 1 ) ) -> ( 0 [,] L ) C_ ( 0 [,] 1 ) )
95 93 19 94 sylancr 
 |-  ( ph -> ( 0 [,] L ) C_ ( 0 [,] 1 ) )
96 95 9 sstrd 
 |-  ( ph -> ( 0 [,] L ) C_ R )
97 96 21 sseldd 
 |-  ( ph -> M e. R )
98 eqid 
 |-  ( Scalar ` H ) = ( Scalar ` H )
99 98 8 clmsubcl 
 |-  ( ( H e. CMod /\ L e. R /\ M e. R ) -> ( L - M ) e. R )
100 91 92 97 99 syl3anc 
 |-  ( ph -> ( L - M ) e. R )
101 98 8 cvsdivcl 
 |-  ( ( H e. CVec /\ ( ( L - M ) e. R /\ M e. R /\ M =/= 0 ) ) -> ( ( L - M ) / M ) e. R )
102 11 100 97 14 101 syl13anc 
 |-  ( ph -> ( ( L - M ) / M ) e. R )
103 9 20 sseldd 
 |-  ( ph -> K e. R )
104 1elunit 
 |-  1 e. ( 0 [,] 1 )
105 104 a1i 
 |-  ( ph -> 1 e. ( 0 [,] 1 ) )
106 9 105 sseldd 
 |-  ( ph -> 1 e. R )
107 98 8 clmsubcl 
 |-  ( ( H e. CMod /\ 1 e. R /\ K e. R ) -> ( 1 - K ) e. R )
108 91 106 103 107 syl3anc 
 |-  ( ph -> ( 1 - K ) e. R )
109 98 8 cvsdivcl 
 |-  ( ( H e. CVec /\ ( K e. R /\ ( 1 - K ) e. R /\ ( 1 - K ) =/= 0 ) ) -> ( K / ( 1 - K ) ) e. R )
110 11 103 108 44 109 syl13anc 
 |-  ( ph -> ( K / ( 1 - K ) ) e. R )
111 clmgrp 
 |-  ( H e. CMod -> H e. Grp )
112 91 111 syl 
 |-  ( ph -> H e. Grp )
113 3 4 grpsubcl 
 |-  ( ( H e. Grp /\ Y e. P /\ X e. P ) -> ( Y .- X ) e. P )
114 112 7 6 113 syl3anc 
 |-  ( ph -> ( Y .- X ) e. P )
115 3 98 5 8 clmvsass 
 |-  ( ( 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 ) ) ) )
116 91 102 110 114 115 syl13anc 
 |-  ( ph -> ( ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) .x. ( Y .- X ) ) = ( ( ( L - M ) / M ) .x. ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) ) )
117 63 recnd 
 |-  ( ph -> ( L - M ) e. CC )
118 117 38 40 42 14 44 divmuldivd 
 |-  ( ph -> ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) = ( ( ( L - M ) x. K ) / ( M x. ( 1 - K ) ) ) )
119 72 41 oveq12d 
 |-  ( ph -> ( ( ( L - M ) x. K ) / ( M x. ( 1 - K ) ) ) = ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) )
120 118 119 eqtrd 
 |-  ( ph -> ( ( ( L - M ) / M ) x. ( K / ( 1 - K ) ) ) = ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) )
121 120 oveq1d 
 |-  ( 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 ) ) )
122 3 4 grpsubcl 
 |-  ( ( H e. Grp /\ X e. P /\ A e. P ) -> ( X .- A ) e. P )
123 112 6 12 122 syl3anc 
 |-  ( ph -> ( X .- A ) e. P )
124 22 oveq2d 
 |-  ( ph -> ( ( 1 - K ) .x. ( X .- A ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
125 40 42 mulcomd 
 |-  ( ph -> ( K x. ( 1 - K ) ) = ( ( 1 - K ) x. K ) )
126 125 oveq1d 
 |-  ( ph -> ( ( K x. ( 1 - K ) ) .x. ( Y .- A ) ) = ( ( ( 1 - K ) x. K ) .x. ( Y .- A ) ) )
127 3 4 grpsubcl 
 |-  ( ( H e. Grp /\ Y e. P /\ A e. P ) -> ( Y .- A ) e. P )
128 112 7 12 127 syl3anc 
 |-  ( ph -> ( Y .- A ) e. P )
129 3 98 5 8 clmvsass 
 |-  ( ( 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 ) ) ) )
130 91 103 108 128 129 syl13anc 
 |-  ( ph -> ( ( K x. ( 1 - K ) ) .x. ( Y .- A ) ) = ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) )
131 3 98 5 8 clmvsass 
 |-  ( ( 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 ) ) ) )
132 91 108 103 128 131 syl13anc 
 |-  ( ph -> ( ( ( 1 - K ) x. K ) .x. ( Y .- A ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
133 126 130 132 3eqtr3d 
 |-  ( ph -> ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) = ( ( 1 - K ) .x. ( K .x. ( Y .- A ) ) ) )
134 eqid 
 |-  ( -g ` ( Scalar ` H ) ) = ( -g ` ( Scalar ` H ) )
135 clmlmod 
 |-  ( H e. CMod -> H e. LMod )
136 91 135 syl 
 |-  ( ph -> H e. LMod )
137 3 5 98 8 4 134 136 106 103 128 lmodsubdir 
 |-  ( ph -> ( ( 1 ( -g ` ( Scalar ` H ) ) K ) .x. ( Y .- A ) ) = ( ( 1 .x. ( Y .- A ) ) .- ( K .x. ( Y .- A ) ) ) )
138 98 8 clmsub 
 |-  ( ( H e. CMod /\ 1 e. R /\ K e. R ) -> ( 1 - K ) = ( 1 ( -g ` ( Scalar ` H ) ) K ) )
139 91 106 103 138 syl3anc 
 |-  ( ph -> ( 1 - K ) = ( 1 ( -g ` ( Scalar ` H ) ) K ) )
140 139 oveq1d 
 |-  ( ph -> ( ( 1 - K ) .x. ( Y .- A ) ) = ( ( 1 ( -g ` ( Scalar ` H ) ) K ) .x. ( Y .- A ) ) )
141 3 5 clmvs1 
 |-  ( ( H e. CMod /\ ( Y .- A ) e. P ) -> ( 1 .x. ( Y .- A ) ) = ( Y .- A ) )
142 91 128 141 syl2anc 
 |-  ( ph -> ( 1 .x. ( Y .- A ) ) = ( Y .- A ) )
143 142 eqcomd 
 |-  ( ph -> ( Y .- A ) = ( 1 .x. ( Y .- A ) ) )
144 143 22 oveq12d 
 |-  ( ph -> ( ( Y .- A ) .- ( X .- A ) ) = ( ( 1 .x. ( Y .- A ) ) .- ( K .x. ( Y .- A ) ) ) )
145 137 140 144 3eqtr4d 
 |-  ( ph -> ( ( 1 - K ) .x. ( Y .- A ) ) = ( ( Y .- A ) .- ( X .- A ) ) )
146 3 4 grpnnncan2 
 |-  ( ( H e. Grp /\ ( Y e. P /\ X e. P /\ A e. P ) ) -> ( ( Y .- A ) .- ( X .- A ) ) = ( Y .- X ) )
147 112 7 6 12 146 syl13anc 
 |-  ( ph -> ( ( Y .- A ) .- ( X .- A ) ) = ( Y .- X ) )
148 145 147 eqtrd 
 |-  ( ph -> ( ( 1 - K ) .x. ( Y .- A ) ) = ( Y .- X ) )
149 148 oveq2d 
 |-  ( ph -> ( K .x. ( ( 1 - K ) .x. ( Y .- A ) ) ) = ( K .x. ( Y .- X ) ) )
150 124 133 149 3eqtr2rd 
 |-  ( ph -> ( K .x. ( Y .- X ) ) = ( ( 1 - K ) .x. ( X .- A ) ) )
151 3 5 98 8 11 103 108 114 123 15 150 cvsmuleqdivd 
 |-  ( ph -> ( Y .- X ) = ( ( ( 1 - K ) / K ) .x. ( X .- A ) ) )
152 3 5 98 8 11 108 103 114 123 44 15 151 cvsdiveqd 
 |-  ( ph -> ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) = ( X .- A ) )
153 152 123 eqeltrd 
 |-  ( ph -> ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) e. P )
154 3 4 grpsubcl 
 |-  ( ( H e. Grp /\ N e. P /\ A e. P ) -> ( N .- A ) e. P )
155 112 13 12 154 syl3anc 
 |-  ( ph -> ( N .- A ) e. P )
156 3 98 5 8 lmodvscl 
 |-  ( ( H e. LMod /\ L e. R /\ ( N .- A ) e. P ) -> ( L .x. ( N .- A ) ) e. P )
157 136 92 155 156 syl3anc 
 |-  ( ph -> ( L .x. ( N .- A ) ) e. P )
158 3 10 grpcl 
 |-  ( ( H e. Grp /\ A e. P /\ ( L .x. ( N .- A ) ) e. P ) -> ( A .+ ( L .x. ( N .- A ) ) ) e. P )
159 112 12 157 158 syl3anc 
 |-  ( ph -> ( A .+ ( L .x. ( N .- A ) ) ) e. P )
160 24 159 eqeltrd 
 |-  ( ph -> B e. P )
161 3 4 grpsubcl 
 |-  ( ( H e. Grp /\ B e. P /\ X e. P ) -> ( B .- X ) e. P )
162 112 160 6 161 syl3anc 
 |-  ( ph -> ( B .- X ) e. P )
163 71 38 17 subne0d 
 |-  ( ph -> ( L - M ) =/= 0 )
164 23 oveq2d 
 |-  ( ph -> ( ( L - M ) .x. ( X .- A ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
165 38 117 mulcomd 
 |-  ( ph -> ( M x. ( L - M ) ) = ( ( L - M ) x. M ) )
166 165 oveq1d 
 |-  ( ph -> ( ( M x. ( L - M ) ) .x. ( N .- A ) ) = ( ( ( L - M ) x. M ) .x. ( N .- A ) ) )
167 3 98 5 8 clmvsass 
 |-  ( ( 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 ) ) ) )
168 91 97 100 155 167 syl13anc 
 |-  ( ph -> ( ( M x. ( L - M ) ) .x. ( N .- A ) ) = ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) )
169 3 98 5 8 clmvsass 
 |-  ( ( 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 ) ) ) )
170 91 100 97 155 169 syl13anc 
 |-  ( ph -> ( ( ( L - M ) x. M ) .x. ( N .- A ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
171 166 168 170 3eqtr3d 
 |-  ( ph -> ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) = ( ( L - M ) .x. ( M .x. ( N .- A ) ) ) )
172 3 5 98 8 4 134 136 92 97 155 lmodsubdir 
 |-  ( ph -> ( ( L ( -g ` ( Scalar ` H ) ) M ) .x. ( N .- A ) ) = ( ( L .x. ( N .- A ) ) .- ( M .x. ( N .- A ) ) ) )
173 98 8 clmsub 
 |-  ( ( H e. CMod /\ L e. R /\ M e. R ) -> ( L - M ) = ( L ( -g ` ( Scalar ` H ) ) M ) )
174 91 92 97 173 syl3anc 
 |-  ( ph -> ( L - M ) = ( L ( -g ` ( Scalar ` H ) ) M ) )
175 174 oveq1d 
 |-  ( ph -> ( ( L - M ) .x. ( N .- A ) ) = ( ( L ( -g ` ( Scalar ` H ) ) M ) .x. ( N .- A ) ) )
176 24 oveq1d 
 |-  ( ph -> ( B .- A ) = ( ( A .+ ( L .x. ( N .- A ) ) ) .- A ) )
177 lmodabl 
 |-  ( H e. LMod -> H e. Abel )
178 136 177 syl 
 |-  ( ph -> H e. Abel )
179 3 10 4 ablpncan2 
 |-  ( ( H e. Abel /\ A e. P /\ ( L .x. ( N .- A ) ) e. P ) -> ( ( A .+ ( L .x. ( N .- A ) ) ) .- A ) = ( L .x. ( N .- A ) ) )
180 178 12 157 179 syl3anc 
 |-  ( ph -> ( ( A .+ ( L .x. ( N .- A ) ) ) .- A ) = ( L .x. ( N .- A ) ) )
181 176 180 eqtrd 
 |-  ( ph -> ( B .- A ) = ( L .x. ( N .- A ) ) )
182 181 23 oveq12d 
 |-  ( ph -> ( ( B .- A ) .- ( X .- A ) ) = ( ( L .x. ( N .- A ) ) .- ( M .x. ( N .- A ) ) ) )
183 172 175 182 3eqtr4d 
 |-  ( ph -> ( ( L - M ) .x. ( N .- A ) ) = ( ( B .- A ) .- ( X .- A ) ) )
184 3 4 grpnnncan2 
 |-  ( ( H e. Grp /\ ( B e. P /\ X e. P /\ A e. P ) ) -> ( ( B .- A ) .- ( X .- A ) ) = ( B .- X ) )
185 112 160 6 12 184 syl13anc 
 |-  ( ph -> ( ( B .- A ) .- ( X .- A ) ) = ( B .- X ) )
186 183 185 eqtrd 
 |-  ( ph -> ( ( L - M ) .x. ( N .- A ) ) = ( B .- X ) )
187 186 oveq2d 
 |-  ( ph -> ( M .x. ( ( L - M ) .x. ( N .- A ) ) ) = ( M .x. ( B .- X ) ) )
188 164 171 187 3eqtr2rd 
 |-  ( ph -> ( M .x. ( B .- X ) ) = ( ( L - M ) .x. ( X .- A ) ) )
189 3 5 98 8 11 97 100 162 123 14 188 cvsmuleqdivd 
 |-  ( ph -> ( B .- X ) = ( ( ( L - M ) / M ) .x. ( X .- A ) ) )
190 3 5 98 8 11 100 97 162 123 163 14 189 cvsdiveqd 
 |-  ( ph -> ( ( M / ( L - M ) ) .x. ( B .- X ) ) = ( X .- A ) )
191 152 190 eqtr4d 
 |-  ( ph -> ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) = ( ( M / ( L - M ) ) .x. ( B .- X ) ) )
192 3 5 98 8 11 97 100 153 162 14 163 191 cvsdiveqd 
 |-  ( ph -> ( ( ( L - M ) / M ) .x. ( ( K / ( 1 - K ) ) .x. ( Y .- X ) ) ) = ( B .- X ) )
193 116 121 192 3eqtr3rd 
 |-  ( ph -> ( B .- X ) = ( ( ( ( L x. K ) - ( M x. K ) ) / ( ( M x. 1 ) - ( M x. K ) ) ) .x. ( Y .- X ) ) )
194 oveq1 
 |-  ( 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 ) ) )
195 194 rspceeqv 
 |-  ( ( ( ( ( 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 ) ) )
196 90 193 195 syl2anc 
 |-  ( ph -> E. k e. ( 0 [,] 1 ) ( B .- X ) = ( k .x. ( Y .- X ) ) )
197 1 2 3 4 5 6 7 11 160 ttgelitv 
 |-  ( ph -> ( B e. ( X I Y ) <-> E. k e. ( 0 [,] 1 ) ( B .- X ) = ( k .x. ( Y .- X ) ) ) )
198 196 197 mpbird 
 |-  ( ph -> B e. ( X I Y ) )