MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttgcontlem1 Structured version   Unicode version

Theorem ttgcontlem1 23146
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.
StepHypRef Expression
1 unitssre 11447 . . . . . . . 8  |-  ( 0 [,] 1 )  C_  RR
2 ttgcontlem1.l . . . . . . . 8  |-  ( ph  ->  L  e.  ( 0 [,] 1 ) )
31, 2sseldi 3369 . . . . . . 7  |-  ( ph  ->  L  e.  RR )
4 ttgcontlem1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( 0 [,] 1 ) )
51, 4sseldi 3369 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
63, 5remulcld 9429 . . . . . 6  |-  ( ph  ->  ( L  x.  K
)  e.  RR )
7 0re 9401 . . . . . . . . 9  |-  0  e.  RR
8 iccssre 11392 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  L  e.  RR )  ->  ( 0 [,] L
)  C_  RR )
97, 3, 8sylancr 663 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] L
)  C_  RR )
10 ttgcontlem1.m . . . . . . . 8  |-  ( ph  ->  M  e.  ( 0 [,] L ) )
119, 10sseldd 3372 . . . . . . 7  |-  ( ph  ->  M  e.  RR )
1211, 5remulcld 9429 . . . . . 6  |-  ( ph  ->  ( M  x.  K
)  e.  RR )
136, 12resubcld 9791 . . . . 5  |-  ( ph  ->  ( ( L  x.  K )  -  ( M  x.  K )
)  e.  RR )
14 1red 9416 . . . . . . 7  |-  ( ph  ->  1  e.  RR )
1511, 14remulcld 9429 . . . . . 6  |-  ( ph  ->  ( M  x.  1 )  e.  RR )
1615, 12resubcld 9791 . . . . 5  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  e.  RR )
1711recnd 9427 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
18 1cnd 9417 . . . . . . 7  |-  ( ph  ->  1  e.  CC )
195recnd 9427 . . . . . . 7  |-  ( ph  ->  K  e.  CC )
2017, 18, 19subdid 9815 . . . . . 6  |-  ( ph  ->  ( M  x.  (
1  -  K ) )  =  ( ( M  x.  1 )  -  ( M  x.  K ) ) )
2118, 19subcld 9734 . . . . . . 7  |-  ( ph  ->  ( 1  -  K
)  e.  CC )
22 ttgcontlem1.o . . . . . . 7  |-  ( ph  ->  M  =/=  0 )
23 ttgcontlem1.q . . . . . . . . 9  |-  ( ph  ->  K  =/=  1 )
2423necomd 2710 . . . . . . . 8  |-  ( ph  ->  1  =/=  K )
2518, 19, 24subne0d 9743 . . . . . . 7  |-  ( ph  ->  ( 1  -  K
)  =/=  0 )
2617, 21, 22, 25mulne0d 10003 . . . . . 6  |-  ( ph  ->  ( M  x.  (
1  -  K ) )  =/=  0 )
2720, 26eqnetrrd 2643 . . . . 5  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  =/=  0 )
2813, 16, 27redivcld 10174 . . . 4  |-  ( ph  ->  ( ( ( L  x.  K )  -  ( M  x.  K
) )  /  (
( M  x.  1 )  -  ( M  x.  K ) ) )  e.  RR )
29 0xr 9445 . . . . . . . . . . 11  |-  0  e.  RR*
3029a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR* )
313rexrd 9448 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR* )
32 iccgelb 11367 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\  L  e.  RR*  /\  M  e.  ( 0 [,] L
) )  ->  0  <_  M )
3330, 31, 10, 32syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  0  <_  M )
3411, 33, 22ne0gt0d 9526 . . . . . . . 8  |-  ( ph  ->  0  <  M )
3511, 34elrpd 11040 . . . . . . 7  |-  ( ph  ->  M  e.  RR+ )
3614rexrd 9448 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR* )
37 iccleub 11366 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  K  e.  ( 0 [,] 1
) )  ->  K  <_  1 )
3830, 36, 4, 37syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  K  <_  1 )
395, 14ltlend 9534 . . . . . . . . 9  |-  ( ph  ->  ( K  <  1  <->  ( K  <_  1  /\  1  =/=  K ) ) )
4038, 24, 39mpbir2and 913 . . . . . . . 8  |-  ( ph  ->  K  <  1 )
41 difrp 11039 . . . . . . . . 9  |-  ( ( K  e.  RR  /\  1  e.  RR )  ->  ( K  <  1  <->  ( 1  -  K )  e.  RR+ ) )
425, 14, 41syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( K  <  1  <->  ( 1  -  K )  e.  RR+ ) )
4340, 42mpbid 210 . . . . . . 7  |-  ( ph  ->  ( 1  -  K
)  e.  RR+ )
4435, 43rpmulcld 11058 . . . . . 6  |-  ( ph  ->  ( M  x.  (
1  -  K ) )  e.  RR+ )
4520, 44eqeltrrd 2518 . . . . 5  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  e.  RR+ )
463, 11resubcld 9791 . . . . . . 7  |-  ( ph  ->  ( L  -  M
)  e.  RR )
47 iccleub 11366 . . . . . . . . 9  |-  ( ( 0  e.  RR*  /\  L  e.  RR*  /\  M  e.  ( 0 [,] L
) )  ->  M  <_  L )
4830, 31, 10, 47syl3anc 1218 . . . . . . . 8  |-  ( ph  ->  M  <_  L )
493, 11subge0d 9944 . . . . . . . 8  |-  ( ph  ->  ( 0  <_  ( L  -  M )  <->  M  <_  L ) )
5048, 49mpbird 232 . . . . . . 7  |-  ( ph  ->  0  <_  ( L  -  M ) )
51 iccgelb 11367 . . . . . . . 8  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  K  e.  ( 0 [,] 1
) )  ->  0  <_  K )
5230, 36, 4, 51syl3anc 1218 . . . . . . 7  |-  ( ph  ->  0  <_  K )
5346, 5, 50, 52mulge0d 9931 . . . . . 6  |-  ( ph  ->  0  <_  ( ( L  -  M )  x.  K ) )
543recnd 9427 . . . . . . 7  |-  ( ph  ->  L  e.  CC )
5554, 17, 19subdird 9816 . . . . . 6  |-  ( ph  ->  ( ( L  -  M )  x.  K
)  =  ( ( L  x.  K )  -  ( M  x.  K ) ) )
5653, 55breqtrd 4331 . . . . 5  |-  ( ph  ->  0  <_  ( ( L  x.  K )  -  ( M  x.  K ) ) )
5713, 45, 56divge0d 11078 . . . 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 )
605, 52, 59ne0gt0d 9526 . . . . . . . . . . 11  |-  ( ph  ->  0  <  K )
615, 60elrpd 11040 . . . . . . . . . 10  |-  ( ph  ->  K  e.  RR+ )
623, 11, 61lemuldivd 11087 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  K )  <_  M  <->  L  <_  ( M  /  K ) ) )
6358, 62mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( L  x.  K
)  <_  M )
6417mulid1d 9418 . . . . . . . 8  |-  ( ph  ->  ( M  x.  1 )  =  M )
6563, 64breqtrrd 4333 . . . . . . 7  |-  ( ph  ->  ( L  x.  K
)  <_  ( M  x.  1 ) )
666, 15, 12, 65lesub1dd 9970 . . . . . 6  |-  ( ph  ->  ( ( L  x.  K )  -  ( M  x.  K )
)  <_  ( ( M  x.  1 )  -  ( M  x.  K ) ) )
6717, 18mulcld 9421 . . . . . . . 8  |-  ( ph  ->  ( M  x.  1 )  e.  CC )
6817, 19mulcld 9421 . . . . . . . 8  |-  ( ph  ->  ( M  x.  K
)  e.  CC )
6967, 68subcld 9734 . . . . . . 7  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  e.  CC )
7069mulid1d 9418 . . . . . 6  |-  ( ph  ->  ( ( ( M  x.  1 )  -  ( M  x.  K
) )  x.  1 )  =  ( ( M  x.  1 )  -  ( M  x.  K ) ) )
7166, 70breqtrrd 4333 . . . . 5  |-  ( ph  ->  ( ( L  x.  K )  -  ( M  x.  K )
)  <_  ( (
( M  x.  1 )  -  ( M  x.  K ) )  x.  1 ) )
7245rpregt0d 11048 . . . . . 6  |-  ( ph  ->  ( ( ( M  x.  1 )  -  ( M  x.  K
) )  e.  RR  /\  0  <  ( ( M  x.  1 )  -  ( M  x.  K ) ) ) )
73 ledivmul 10220 . . . . . 6  |-  ( ( ( ( L  x.  K )  -  ( M  x.  K )
)  e.  RR  /\  1  e.  RR  /\  (
( ( M  x.  1 )  -  ( M  x.  K )
)  e.  RR  /\  0  <  ( ( M  x.  1 )  -  ( M  x.  K
) ) ) )  ->  ( ( ( ( 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 ) ) )
7413, 14, 72, 73syl3anc 1218 . . . . 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 ) ) )
7571, 74mpbird 232 . . . 4  |-  ( ph  ->  ( ( ( L  x.  K )  -  ( M  x.  K
) )  /  (
( M  x.  1 )  -  ( M  x.  K ) ) )  <_  1 )
76 1re 9400 . . . . 5  |-  1  e.  RR
777, 76elicc2i 11376 . . . 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 ) )
7828, 57, 75, 77syl3anbrc 1172 . . 3  |-  ( ph  ->  ( ( ( L  x.  K )  -  ( M  x.  K
) )  /  (
( M  x.  1 )  -  ( M  x.  K ) ) )  e.  ( 0 [,] 1 ) )
79 ttgcontlem1.h . . . . . 6  |-  ( ph  ->  H  e. CVec )
8079cvsclm 20694 . . . . 5  |-  ( ph  ->  H  e. CMod )
81 ttgbtwnid.2 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] 1
)  C_  R )
8281, 2sseldd 3372 . . . . . . 7  |-  ( ph  ->  L  e.  R )
83 0elunit 11418 . . . . . . . . . 10  |-  0  e.  ( 0 [,] 1
)
84 iccss2 11381 . . . . . . . . . 10  |-  ( ( 0  e.  ( 0 [,] 1 )  /\  L  e.  ( 0 [,] 1 ) )  ->  ( 0 [,] L )  C_  (
0 [,] 1 ) )
8583, 2, 84sylancr 663 . . . . . . . . 9  |-  ( ph  ->  ( 0 [,] L
)  C_  ( 0 [,] 1 ) )
8685, 81sstrd 3381 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] L
)  C_  R )
8786, 10sseldd 3372 . . . . . . 7  |-  ( ph  ->  M  e.  R )
88 eqid 2443 . . . . . . . 8  |-  (Scalar `  H )  =  (Scalar `  H )
89 ttgbtwnid.r . . . . . . . 8  |-  R  =  ( Base `  (Scalar `  H ) )
9088, 89clmsubcl 20672 . . . . . . 7  |-  ( ( H  e. CMod  /\  L  e.  R  /\  M  e.  R )  ->  ( L  -  M )  e.  R )
9180, 82, 87, 90syl3anc 1218 . . . . . 6  |-  ( ph  ->  ( L  -  M
)  e.  R )
9288, 89cvsdivcl 20697 . . . . . 6  |-  ( ( H  e. CVec  /\  (
( L  -  M
)  e.  R  /\  M  e.  R  /\  M  =/=  0 ) )  ->  ( ( L  -  M )  /  M )  e.  R
)
9379, 91, 87, 22, 92syl13anc 1220 . . . . 5  |-  ( ph  ->  ( ( L  -  M )  /  M
)  e.  R )
9481, 4sseldd 3372 . . . . . 6  |-  ( ph  ->  K  e.  R )
95 1elunit 11419 . . . . . . . . 9  |-  1  e.  ( 0 [,] 1
)
9695a1i 11 . . . . . . . 8  |-  ( ph  ->  1  e.  ( 0 [,] 1 ) )
9781, 96sseldd 3372 . . . . . . 7  |-  ( ph  ->  1  e.  R )
9888, 89clmsubcl 20672 . . . . . . 7  |-  ( ( H  e. CMod  /\  1  e.  R  /\  K  e.  R )  ->  (
1  -  K )  e.  R )
9980, 97, 94, 98syl3anc 1218 . . . . . 6  |-  ( ph  ->  ( 1  -  K
)  e.  R )
10088, 89cvsdivcl 20697 . . . . . 6  |-  ( ( H  e. CVec  /\  ( K  e.  R  /\  ( 1  -  K
)  e.  R  /\  ( 1  -  K
)  =/=  0 ) )  ->  ( K  /  ( 1  -  K ) )  e.  R )
10179, 94, 99, 25, 100syl13anc 1220 . . . . 5  |-  ( ph  ->  ( K  /  (
1  -  K ) )  e.  R )
102 clmgrp 20655 . . . . . . 7  |-  ( H  e. CMod  ->  H  e.  Grp )
10380, 102syl 16 . . . . . 6  |-  ( ph  ->  H  e.  Grp )
104 ttgelitv.y . . . . . 6  |-  ( ph  ->  Y  e.  P )
105 ttgelitv.x . . . . . 6  |-  ( ph  ->  X  e.  P )
106 ttgitvval.b . . . . . . 7  |-  P  =  ( Base `  H
)
107 ttgitvval.m . . . . . . 7  |-  .-  =  ( -g `  H )
108106, 107grpsubcl 15621 . . . . . 6  |-  ( ( H  e.  Grp  /\  Y  e.  P  /\  X  e.  P )  ->  ( Y  .-  X
)  e.  P )
109103, 104, 105, 108syl3anc 1218 . . . . 5  |-  ( ph  ->  ( Y  .-  X
)  e.  P )
110 ttgitvval.s . . . . . 6  |-  .x.  =  ( .s `  H )
111106, 88, 110, 89clmvsass 20674 . . . . 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 ) ) ) )
11280, 93, 101, 109, 111syl13anc 1220 . . . 4  |-  ( ph  ->  ( ( ( ( L  -  M )  /  M )  x.  ( K  /  (
1  -  K ) ) )  .x.  ( Y  .-  X ) )  =  ( ( ( L  -  M )  /  M )  .x.  ( ( K  / 
( 1  -  K
) )  .x.  ( Y  .-  X ) ) ) )
11346recnd 9427 . . . . . . 7  |-  ( ph  ->  ( L  -  M
)  e.  CC )
114113, 17, 19, 21, 22, 25divmuldivd 10163 . . . . . 6  |-  ( ph  ->  ( ( ( L  -  M )  /  M )  x.  ( K  /  ( 1  -  K ) ) )  =  ( ( ( L  -  M )  x.  K )  / 
( M  x.  (
1  -  K ) ) ) )
11555, 20oveq12d 6124 . . . . . 6  |-  ( ph  ->  ( ( ( L  -  M )  x.  K )  /  ( M  x.  ( 1  -  K ) ) )  =  ( ( ( L  x.  K
)  -  ( M  x.  K ) )  /  ( ( M  x.  1 )  -  ( M  x.  K
) ) ) )
116114, 115eqtrd 2475 . . . . 5  |-  ( ph  ->  ( ( ( L  -  M )  /  M )  x.  ( K  /  ( 1  -  K ) ) )  =  ( ( ( L  x.  K )  -  ( M  x.  K ) )  / 
( ( M  x.  1 )  -  ( M  x.  K )
) ) )
117116oveq1d 6121 . . . 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 ) ) )
118 ttgcontlem1.a . . . . . . . 8  |-  ( ph  ->  A  e.  P )
119106, 107grpsubcl 15621 . . . . . . . 8  |-  ( ( H  e.  Grp  /\  X  e.  P  /\  A  e.  P )  ->  ( X  .-  A
)  e.  P )
120103, 105, 118, 119syl3anc 1218 . . . . . . 7  |-  ( ph  ->  ( X  .-  A
)  e.  P )
121 ttgcontlem1.y . . . . . . . . . 10  |-  ( ph  ->  ( X  .-  A
)  =  ( K 
.x.  ( Y  .-  A ) ) )
122121oveq2d 6122 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( X  .-  A ) )  =  ( ( 1  -  K )  .x.  ( K  .x.  ( Y 
.-  A ) ) ) )
12319, 21mulcomd 9422 . . . . . . . . . . 11  |-  ( ph  ->  ( K  x.  (
1  -  K ) )  =  ( ( 1  -  K )  x.  K ) )
124123oveq1d 6121 . . . . . . . . . 10  |-  ( ph  ->  ( ( K  x.  ( 1  -  K
) )  .x.  ( Y  .-  A ) )  =  ( ( ( 1  -  K )  x.  K )  .x.  ( Y  .-  A ) ) )
125106, 107grpsubcl 15621 . . . . . . . . . . . 12  |-  ( ( H  e.  Grp  /\  Y  e.  P  /\  A  e.  P )  ->  ( Y  .-  A
)  e.  P )
126103, 104, 118, 125syl3anc 1218 . . . . . . . . . . 11  |-  ( ph  ->  ( Y  .-  A
)  e.  P )
127106, 88, 110, 89clmvsass 20674 . . . . . . . . . . 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 ) ) ) )
12880, 94, 99, 126, 127syl13anc 1220 . . . . . . . . . 10  |-  ( ph  ->  ( ( K  x.  ( 1  -  K
) )  .x.  ( Y  .-  A ) )  =  ( K  .x.  ( ( 1  -  K )  .x.  ( Y  .-  A ) ) ) )
129106, 88, 110, 89clmvsass 20674 . . . . . . . . . . 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 ) ) ) )
13080, 99, 94, 126, 129syl13anc 1220 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 1  -  K )  x.  K )  .x.  ( Y  .-  A ) )  =  ( ( 1  -  K )  .x.  ( K  .x.  ( Y 
.-  A ) ) ) )
131124, 128, 1303eqtr3d 2483 . . . . . . . . 9  |-  ( ph  ->  ( K  .x.  (
( 1  -  K
)  .x.  ( Y  .-  A ) ) )  =  ( ( 1  -  K )  .x.  ( K  .x.  ( Y 
.-  A ) ) ) )
132 eqid 2443 . . . . . . . . . . . . 13  |-  ( -g `  (Scalar `  H )
)  =  ( -g `  (Scalar `  H )
)
133 clmlmod 20654 . . . . . . . . . . . . . 14  |-  ( H  e. CMod  ->  H  e.  LMod )
13480, 133syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  H  e.  LMod )
135106, 110, 88, 89, 107, 132, 134, 97, 94, 126lmodsubdir 17018 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 (
-g `  (Scalar `  H
) ) K ) 
.x.  ( Y  .-  A ) )  =  ( ( 1  .x.  ( Y  .-  A
) )  .-  ( K  .x.  ( Y  .-  A ) ) ) )
13688, 89clmsub 20667 . . . . . . . . . . . . . 14  |-  ( ( H  e. CMod  /\  1  e.  R  /\  K  e.  R )  ->  (
1  -  K )  =  ( 1 (
-g `  (Scalar `  H
) ) K ) )
13780, 97, 94, 136syl3anc 1218 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  -  K
)  =  ( 1 ( -g `  (Scalar `  H ) ) K ) )
138137oveq1d 6121 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( Y  .-  A ) )  =  ( ( 1 ( -g `  (Scalar `  H ) ) K )  .x.  ( Y 
.-  A ) ) )
139106, 110clmvs1 20676 . . . . . . . . . . . . . . 15  |-  ( ( H  e. CMod  /\  ( Y  .-  A )  e.  P )  ->  (
1  .x.  ( Y  .-  A ) )  =  ( Y  .-  A
) )
14080, 126, 139syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  .x.  ( Y  .-  A ) )  =  ( Y  .-  A ) )
141140eqcomd 2448 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y  .-  A
)  =  ( 1 
.x.  ( Y  .-  A ) ) )
142141, 121oveq12d 6124 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Y  .-  A )  .-  ( X  .-  A ) )  =  ( ( 1 
.x.  ( Y  .-  A ) )  .-  ( K  .x.  ( Y 
.-  A ) ) ) )
143135, 138, 1423eqtr4d 2485 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( Y  .-  A ) )  =  ( ( Y 
.-  A )  .-  ( X  .-  A ) ) )
144106, 107grpnnncan2 15636 . . . . . . . . . . . 12  |-  ( ( H  e.  Grp  /\  ( Y  e.  P  /\  X  e.  P  /\  A  e.  P
) )  ->  (
( Y  .-  A
)  .-  ( X  .-  A ) )  =  ( Y  .-  X
) )
145103, 104, 105, 118, 144syl13anc 1220 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Y  .-  A )  .-  ( X  .-  A ) )  =  ( Y  .-  X ) )
146143, 145eqtrd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( Y  .-  A ) )  =  ( Y  .-  X ) )
147146oveq2d 6122 . . . . . . . . 9  |-  ( ph  ->  ( K  .x.  (
( 1  -  K
)  .x.  ( Y  .-  A ) ) )  =  ( K  .x.  ( Y  .-  X ) ) )
148122, 131, 1473eqtr2rd 2482 . . . . . . . 8  |-  ( ph  ->  ( K  .x.  ( Y  .-  X ) )  =  ( ( 1  -  K )  .x.  ( X  .-  A ) ) )
149106, 110, 88, 89, 79, 94, 99, 109, 120, 59, 148cvsmuleqdivd 20698 . . . . . . 7  |-  ( ph  ->  ( Y  .-  X
)  =  ( ( ( 1  -  K
)  /  K ) 
.x.  ( X  .-  A ) ) )
150106, 110, 88, 89, 79, 99, 94, 109, 120, 25, 59, 149cvsdiveqd 20699 . . . . . 6  |-  ( ph  ->  ( ( K  / 
( 1  -  K
) )  .x.  ( Y  .-  X ) )  =  ( X  .-  A ) )
151150, 120eqeltrd 2517 . . . . 5  |-  ( ph  ->  ( ( K  / 
( 1  -  K
) )  .x.  ( Y  .-  X ) )  e.  P )
152 ttgcontlem1.b . . . . . . 7  |-  ( ph  ->  B  =  ( A 
.+  ( L  .x.  ( N  .-  A ) ) ) )
153 ttgcontlem1.n . . . . . . . . . 10  |-  ( ph  ->  N  e.  P )
154106, 107grpsubcl 15621 . . . . . . . . . 10  |-  ( ( H  e.  Grp  /\  N  e.  P  /\  A  e.  P )  ->  ( N  .-  A
)  e.  P )
155103, 153, 118, 154syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  ( N  .-  A
)  e.  P )
156106, 88, 110, 89lmodvscl 16980 . . . . . . . . 9  |-  ( ( H  e.  LMod  /\  L  e.  R  /\  ( N  .-  A )  e.  P )  ->  ( L  .x.  ( N  .-  A ) )  e.  P )
157134, 82, 155, 156syl3anc 1218 . . . . . . . 8  |-  ( ph  ->  ( L  .x.  ( N  .-  A ) )  e.  P )
158 ttgitvval.p . . . . . . . . 9  |-  .+  =  ( +g  `  H )
159106, 158grpcl 15566 . . . . . . . 8  |-  ( ( H  e.  Grp  /\  A  e.  P  /\  ( L  .x.  ( N 
.-  A ) )  e.  P )  -> 
( A  .+  ( L  .x.  ( N  .-  A ) ) )  e.  P )
160103, 118, 157, 159syl3anc 1218 . . . . . . 7  |-  ( ph  ->  ( A  .+  ( L  .x.  ( N  .-  A ) ) )  e.  P )
161152, 160eqeltrd 2517 . . . . . 6  |-  ( ph  ->  B  e.  P )
162106, 107grpsubcl 15621 . . . . . 6  |-  ( ( H  e.  Grp  /\  B  e.  P  /\  X  e.  P )  ->  ( B  .-  X
)  e.  P )
163103, 161, 105, 162syl3anc 1218 . . . . 5  |-  ( ph  ->  ( B  .-  X
)  e.  P )
164 ttgcontlem1.r . . . . . 6  |-  ( ph  ->  L  =/=  M )
16554, 17, 164subne0d 9743 . . . . 5  |-  ( ph  ->  ( L  -  M
)  =/=  0 )
166 ttgcontlem1.x . . . . . . . . . 10  |-  ( ph  ->  ( X  .-  A
)  =  ( M 
.x.  ( N  .-  A ) ) )
167166oveq2d 6122 . . . . . . . . 9  |-  ( ph  ->  ( ( L  -  M )  .x.  ( X  .-  A ) )  =  ( ( L  -  M )  .x.  ( M  .x.  ( N 
.-  A ) ) ) )
16817, 113mulcomd 9422 . . . . . . . . . . 11  |-  ( ph  ->  ( M  x.  ( L  -  M )
)  =  ( ( L  -  M )  x.  M ) )
169168oveq1d 6121 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  x.  ( L  -  M
) )  .x.  ( N  .-  A ) )  =  ( ( ( L  -  M )  x.  M )  .x.  ( N  .-  A ) ) )
170106, 88, 110, 89clmvsass 20674 . . . . . . . . . . 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 ) ) ) )
17180, 87, 91, 155, 170syl13anc 1220 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  x.  ( L  -  M
) )  .x.  ( N  .-  A ) )  =  ( M  .x.  ( ( L  -  M )  .x.  ( N  .-  A ) ) ) )
172106, 88, 110, 89clmvsass 20674 . . . . . . . . . . 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 ) ) ) )
17380, 91, 87, 155, 172syl13anc 1220 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  -  M )  x.  M )  .x.  ( N  .-  A ) )  =  ( ( L  -  M )  .x.  ( M  .x.  ( N 
.-  A ) ) ) )
174169, 171, 1733eqtr3d 2483 . . . . . . . . 9  |-  ( ph  ->  ( M  .x.  (
( L  -  M
)  .x.  ( N  .-  A ) ) )  =  ( ( L  -  M )  .x.  ( M  .x.  ( N 
.-  A ) ) ) )
175106, 110, 88, 89, 107, 132, 134, 82, 87, 155lmodsubdir 17018 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L (
-g `  (Scalar `  H
) ) M ) 
.x.  ( N  .-  A ) )  =  ( ( L  .x.  ( N  .-  A ) )  .-  ( M 
.x.  ( N  .-  A ) ) ) )
17688, 89clmsub 20667 . . . . . . . . . . . . . 14  |-  ( ( H  e. CMod  /\  L  e.  R  /\  M  e.  R )  ->  ( L  -  M )  =  ( L (
-g `  (Scalar `  H
) ) M ) )
17780, 82, 87, 176syl3anc 1218 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  M
)  =  ( L ( -g `  (Scalar `  H ) ) M ) )
178177oveq1d 6121 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  -  M )  .x.  ( N  .-  A ) )  =  ( ( L ( -g `  (Scalar `  H ) ) M )  .x.  ( N 
.-  A ) ) )
179152oveq1d 6121 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  .-  A
)  =  ( ( A  .+  ( L 
.x.  ( N  .-  A ) ) ) 
.-  A ) )
180 lmodabl 17007 . . . . . . . . . . . . . . . 16  |-  ( H  e.  LMod  ->  H  e. 
Abel )
181134, 180syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H  e.  Abel )
182106, 158, 107ablpncan2 16320 . . . . . . . . . . . . . . 15  |-  ( ( H  e.  Abel  /\  A  e.  P  /\  ( L  .x.  ( N  .-  A ) )  e.  P )  ->  (
( A  .+  ( L  .x.  ( N  .-  A ) ) ) 
.-  A )  =  ( L  .x.  ( N  .-  A ) ) )
183181, 118, 157, 182syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  .+  ( L  .x.  ( N 
.-  A ) ) )  .-  A )  =  ( L  .x.  ( N  .-  A ) ) )
184179, 183eqtrd 2475 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  .-  A
)  =  ( L 
.x.  ( N  .-  A ) ) )
185184, 166oveq12d 6124 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  .-  A )  .-  ( X  .-  A ) )  =  ( ( L 
.x.  ( N  .-  A ) )  .-  ( M  .x.  ( N 
.-  A ) ) ) )
186175, 178, 1853eqtr4d 2485 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  -  M )  .x.  ( N  .-  A ) )  =  ( ( B 
.-  A )  .-  ( X  .-  A ) ) )
187106, 107grpnnncan2 15636 . . . . . . . . . . . 12  |-  ( ( H  e.  Grp  /\  ( B  e.  P  /\  X  e.  P  /\  A  e.  P
) )  ->  (
( B  .-  A
)  .-  ( X  .-  A ) )  =  ( B  .-  X
) )
188103, 161, 105, 118, 187syl13anc 1220 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  .-  A )  .-  ( X  .-  A ) )  =  ( B  .-  X ) )
189186, 188eqtrd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  -  M )  .x.  ( N  .-  A ) )  =  ( B  .-  X ) )
190189oveq2d 6122 . . . . . . . . 9  |-  ( ph  ->  ( M  .x.  (
( L  -  M
)  .x.  ( N  .-  A ) ) )  =  ( M  .x.  ( B  .-  X ) ) )
191167, 174, 1903eqtr2rd 2482 . . . . . . . 8  |-  ( ph  ->  ( M  .x.  ( B  .-  X ) )  =  ( ( L  -  M )  .x.  ( X  .-  A ) ) )
192106, 110, 88, 89, 79, 87, 91, 163, 120, 22, 191cvsmuleqdivd 20698 . . . . . . 7  |-  ( ph  ->  ( B  .-  X
)  =  ( ( ( L  -  M
)  /  M ) 
.x.  ( X  .-  A ) ) )
193106, 110, 88, 89, 79, 91, 87, 163, 120, 165, 22, 192cvsdiveqd 20699 . . . . . 6  |-  ( ph  ->  ( ( M  / 
( L  -  M
) )  .x.  ( B  .-  X ) )  =  ( X  .-  A ) )
194150, 193eqtr4d 2478 . . . . 5  |-  ( ph  ->  ( ( K  / 
( 1  -  K
) )  .x.  ( Y  .-  X ) )  =  ( ( M  /  ( L  -  M ) )  .x.  ( B  .-  X ) ) )
195106, 110, 88, 89, 79, 87, 91, 151, 163, 22, 165, 194cvsdiveqd 20699 . . . 4  |-  ( ph  ->  ( ( ( L  -  M )  /  M )  .x.  (
( K  /  (
1  -  K ) )  .x.  ( Y 
.-  X ) ) )  =  ( B 
.-  X ) )
196112, 117, 1953eqtr3rd 2484 . . 3  |-  ( ph  ->  ( B  .-  X
)  =  ( ( ( ( L  x.  K )  -  ( M  x.  K )
)  /  ( ( M  x.  1 )  -  ( M  x.  K ) ) ) 
.x.  ( Y  .-  X ) ) )
197 oveq1 6113 . . . . 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 ) ) )
198197eqeq2d 2454 . . . 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 ) ) ) )
199198rspcev 3088 . . 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 ) ) )
20078, 196, 199syl2anc 661 . 2  |-  ( ph  ->  E. k  e.  ( 0 [,] 1 ) ( B  .-  X
)  =  ( k 
.x.  ( Y  .-  X ) ) )
201 ttgval.n . . 3  |-  G  =  (toTG `  H )
202 ttgitvval.i . . 3  |-  I  =  (Itv `  G )
203201, 202, 106, 107, 110, 105, 104, 80, 161ttgelitv 23144 . 2  |-  ( ph  ->  ( B  e.  ( X I Y )  <->  E. k  e.  (
0 [,] 1 ) ( B  .-  X
)  =  ( k 
.x.  ( Y  .-  X ) ) ) )
204200, 203mpbird 232 1  |-  ( ph  ->  B  e.  ( X I Y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2620   E.wrex 2731    C_ wss 3343   class class class wbr 4307   ` cfv 5433  (class class class)co 6106   RRcr 9296   0cc0 9297   1c1 9298    x. cmul 9302   RR*cxr 9432    < clt 9433    <_ cle 9434    - cmin 9610    / cdiv 10008   RR+crp 11006   [,]cicc 11318   Basecbs 14189   +g cplusg 14253  Scalarcsca 14256   .scvsca 14257   Grpcgrp 15425   -gcsg 15428   Abelcabel 16293   LModclmod 16963  CModcclm 20649  CVecccvs 20691  Itvcitv 22912  toTGcttg 23134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-addf 9376  ax-mulf 9377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-1st 6592  df-2nd 6593  df-tpos 6760  df-recs 6847  df-rdg 6881  df-1o 6935  df-oadd 6939  df-er 7116  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-div 10009  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-5 10398  df-6 10399  df-7 10400  df-8 10401  df-9 10402  df-10 10403  df-n0 10595  df-z 10662  df-dec 10771  df-uz 10877  df-rp 11007  df-icc 11322  df-fz 11453  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-sets 14195  df-ress 14196  df-plusg 14266  df-mulr 14267  df-starv 14268  df-tset 14272  df-ple 14273  df-ds 14275  df-unif 14276  df-0g 14395  df-mnd 15430  df-grp 15560  df-minusg 15561  df-sbg 15562  df-subg 15693  df-cmn 16294  df-abl 16295  df-mgp 16607  df-ur 16619  df-rng 16662  df-cring 16663  df-oppr 16730  df-dvdsr 16748  df-unit 16749  df-invr 16779  df-dvr 16790  df-drng 16849  df-subrg 16878  df-lmod 16965  df-lvec 17199  df-cnfld 17834  df-clm 20650  df-cvs 20692  df-itv 22914  df-lng 22915  df-ttg 23135
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator