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

Theorem ttgcontlem1 23066
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 11428 . . . . . . . 8  |-  ( 0 [,] 1 )  C_  RR
2 ttgcontlem1.l . . . . . . . 8  |-  ( ph  ->  L  e.  ( 0 [,] 1 ) )
31, 2sseldi 3351 . . . . . . 7  |-  ( ph  ->  L  e.  RR )
4 ttgcontlem1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( 0 [,] 1 ) )
51, 4sseldi 3351 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
63, 5remulcld 9410 . . . . . 6  |-  ( ph  ->  ( L  x.  K
)  e.  RR )
7 0re 9382 . . . . . . . . 9  |-  0  e.  RR
8 iccssre 11373 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  L  e.  RR )  ->  ( 0 [,] L
)  C_  RR )
97, 3, 8sylancr 658 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] L
)  C_  RR )
10 ttgcontlem1.m . . . . . . . 8  |-  ( ph  ->  M  e.  ( 0 [,] L ) )
119, 10sseldd 3354 . . . . . . 7  |-  ( ph  ->  M  e.  RR )
1211, 5remulcld 9410 . . . . . 6  |-  ( ph  ->  ( M  x.  K
)  e.  RR )
136, 12resubcld 9772 . . . . 5  |-  ( ph  ->  ( ( L  x.  K )  -  ( M  x.  K )
)  e.  RR )
14 1red 9397 . . . . . . 7  |-  ( ph  ->  1  e.  RR )
1511, 14remulcld 9410 . . . . . 6  |-  ( ph  ->  ( M  x.  1 )  e.  RR )
1615, 12resubcld 9772 . . . . 5  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  e.  RR )
1711recnd 9408 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
18 1cnd 9398 . . . . . . 7  |-  ( ph  ->  1  e.  CC )
195recnd 9408 . . . . . . 7  |-  ( ph  ->  K  e.  CC )
2017, 18, 19subdid 9796 . . . . . 6  |-  ( ph  ->  ( M  x.  (
1  -  K ) )  =  ( ( M  x.  1 )  -  ( M  x.  K ) ) )
2118, 19subcld 9715 . . . . . . 7  |-  ( ph  ->  ( 1  -  K
)  e.  CC )
22 ttgcontlem1.o . . . . . . 7  |-  ( ph  ->  M  =/=  0 )
23 ttgcontlem1.q . . . . . . . . 9  |-  ( ph  ->  K  =/=  1 )
2423necomd 2693 . . . . . . . 8  |-  ( ph  ->  1  =/=  K )
2518, 19, 24subne0d 9724 . . . . . . 7  |-  ( ph  ->  ( 1  -  K
)  =/=  0 )
2617, 21, 22, 25mulne0d 9984 . . . . . 6  |-  ( ph  ->  ( M  x.  (
1  -  K ) )  =/=  0 )
2720, 26eqnetrrd 2626 . . . . 5  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  =/=  0 )
2813, 16, 27redivcld 10155 . . . 4  |-  ( ph  ->  ( ( ( L  x.  K )  -  ( M  x.  K
) )  /  (
( M  x.  1 )  -  ( M  x.  K ) ) )  e.  RR )
29 0xr 9426 . . . . . . . . . . 11  |-  0  e.  RR*
3029a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR* )
313rexrd 9429 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR* )
32 iccgelb 11348 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\  L  e.  RR*  /\  M  e.  ( 0 [,] L
) )  ->  0  <_  M )
3330, 31, 10, 32syl3anc 1213 . . . . . . . . 9  |-  ( ph  ->  0  <_  M )
3411, 33, 22ne0gt0d 9507 . . . . . . . 8  |-  ( ph  ->  0  <  M )
3511, 34elrpd 11021 . . . . . . 7  |-  ( ph  ->  M  e.  RR+ )
3614rexrd 9429 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR* )
37 iccleub 11347 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  K  e.  ( 0 [,] 1
) )  ->  K  <_  1 )
3830, 36, 4, 37syl3anc 1213 . . . . . . . . 9  |-  ( ph  ->  K  <_  1 )
395, 14ltlend 9515 . . . . . . . . 9  |-  ( ph  ->  ( K  <  1  <->  ( K  <_  1  /\  1  =/=  K ) ) )
4038, 24, 39mpbir2and 908 . . . . . . . 8  |-  ( ph  ->  K  <  1 )
41 difrp 11020 . . . . . . . . 9  |-  ( ( K  e.  RR  /\  1  e.  RR )  ->  ( K  <  1  <->  ( 1  -  K )  e.  RR+ ) )
425, 14, 41syl2anc 656 . . . . . . . 8  |-  ( ph  ->  ( K  <  1  <->  ( 1  -  K )  e.  RR+ ) )
4340, 42mpbid 210 . . . . . . 7  |-  ( ph  ->  ( 1  -  K
)  e.  RR+ )
4435, 43rpmulcld 11039 . . . . . 6  |-  ( ph  ->  ( M  x.  (
1  -  K ) )  e.  RR+ )
4520, 44eqeltrrd 2516 . . . . 5  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  e.  RR+ )
463, 11resubcld 9772 . . . . . . 7  |-  ( ph  ->  ( L  -  M
)  e.  RR )
47 iccleub 11347 . . . . . . . . 9  |-  ( ( 0  e.  RR*  /\  L  e.  RR*  /\  M  e.  ( 0 [,] L
) )  ->  M  <_  L )
4830, 31, 10, 47syl3anc 1213 . . . . . . . 8  |-  ( ph  ->  M  <_  L )
493, 11subge0d 9925 . . . . . . . 8  |-  ( ph  ->  ( 0  <_  ( L  -  M )  <->  M  <_  L ) )
5048, 49mpbird 232 . . . . . . 7  |-  ( ph  ->  0  <_  ( L  -  M ) )
51 iccgelb 11348 . . . . . . . 8  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  K  e.  ( 0 [,] 1
) )  ->  0  <_  K )
5230, 36, 4, 51syl3anc 1213 . . . . . . 7  |-  ( ph  ->  0  <_  K )
5346, 5, 50, 52mulge0d 9912 . . . . . 6  |-  ( ph  ->  0  <_  ( ( L  -  M )  x.  K ) )
543recnd 9408 . . . . . . 7  |-  ( ph  ->  L  e.  CC )
5554, 17, 19subdird 9797 . . . . . 6  |-  ( ph  ->  ( ( L  -  M )  x.  K
)  =  ( ( L  x.  K )  -  ( M  x.  K ) ) )
5653, 55breqtrd 4313 . . . . 5  |-  ( ph  ->  0  <_  ( ( L  x.  K )  -  ( M  x.  K ) ) )
5713, 45, 56divge0d 11059 . . . 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 9507 . . . . . . . . . . 11  |-  ( ph  ->  0  <  K )
615, 60elrpd 11021 . . . . . . . . . 10  |-  ( ph  ->  K  e.  RR+ )
623, 11, 61lemuldivd 11068 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  K )  <_  M  <->  L  <_  ( M  /  K ) ) )
6358, 62mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( L  x.  K
)  <_  M )
6417mulid1d 9399 . . . . . . . 8  |-  ( ph  ->  ( M  x.  1 )  =  M )
6563, 64breqtrrd 4315 . . . . . . 7  |-  ( ph  ->  ( L  x.  K
)  <_  ( M  x.  1 ) )
666, 15, 12, 65lesub1dd 9951 . . . . . 6  |-  ( ph  ->  ( ( L  x.  K )  -  ( M  x.  K )
)  <_  ( ( M  x.  1 )  -  ( M  x.  K ) ) )
6717, 18mulcld 9402 . . . . . . . 8  |-  ( ph  ->  ( M  x.  1 )  e.  CC )
6817, 19mulcld 9402 . . . . . . . 8  |-  ( ph  ->  ( M  x.  K
)  e.  CC )
6967, 68subcld 9715 . . . . . . 7  |-  ( ph  ->  ( ( M  x.  1 )  -  ( M  x.  K )
)  e.  CC )
7069mulid1d 9399 . . . . . 6  |-  ( ph  ->  ( ( ( M  x.  1 )  -  ( M  x.  K
) )  x.  1 )  =  ( ( M  x.  1 )  -  ( M  x.  K ) ) )
7166, 70breqtrrd 4315 . . . . 5  |-  ( ph  ->  ( ( L  x.  K )  -  ( M  x.  K )
)  <_  ( (
( M  x.  1 )  -  ( M  x.  K ) )  x.  1 ) )
7245rpregt0d 11029 . . . . . 6  |-  ( ph  ->  ( ( ( M  x.  1 )  -  ( M  x.  K
) )  e.  RR  /\  0  <  ( ( M  x.  1 )  -  ( M  x.  K ) ) ) )
73 ledivmul 10201 . . . . . 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 1213 . . . . 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 9381 . . . . 5  |-  1  e.  RR
777, 76elicc2i 11357 . . . 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 1167 . . 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 20638 . . . . 5  |-  ( ph  ->  H  e. CMod )
81 ttgbtwnid.2 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] 1
)  C_  R )
8281, 2sseldd 3354 . . . . . . 7  |-  ( ph  ->  L  e.  R )
83 0elunit 11399 . . . . . . . . . 10  |-  0  e.  ( 0 [,] 1
)
84 iccss2 11362 . . . . . . . . . 10  |-  ( ( 0  e.  ( 0 [,] 1 )  /\  L  e.  ( 0 [,] 1 ) )  ->  ( 0 [,] L )  C_  (
0 [,] 1 ) )
8583, 2, 84sylancr 658 . . . . . . . . 9  |-  ( ph  ->  ( 0 [,] L
)  C_  ( 0 [,] 1 ) )
8685, 81sstrd 3363 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] L
)  C_  R )
8786, 10sseldd 3354 . . . . . . 7  |-  ( ph  ->  M  e.  R )
88 eqid 2441 . . . . . . . 8  |-  (Scalar `  H )  =  (Scalar `  H )
89 ttgbtwnid.r . . . . . . . 8  |-  R  =  ( Base `  (Scalar `  H ) )
9088, 89clmsubcl 20616 . . . . . . 7  |-  ( ( H  e. CMod  /\  L  e.  R  /\  M  e.  R )  ->  ( L  -  M )  e.  R )
9180, 82, 87, 90syl3anc 1213 . . . . . 6  |-  ( ph  ->  ( L  -  M
)  e.  R )
9288, 89cvsdivcl 20641 . . . . . 6  |-  ( ( H  e. CVec  /\  (
( L  -  M
)  e.  R  /\  M  e.  R  /\  M  =/=  0 ) )  ->  ( ( L  -  M )  /  M )  e.  R
)
9379, 91, 87, 22, 92syl13anc 1215 . . . . 5  |-  ( ph  ->  ( ( L  -  M )  /  M
)  e.  R )
9481, 4sseldd 3354 . . . . . 6  |-  ( ph  ->  K  e.  R )
95 1elunit 11400 . . . . . . . . 9  |-  1  e.  ( 0 [,] 1
)
9695a1i 11 . . . . . . . 8  |-  ( ph  ->  1  e.  ( 0 [,] 1 ) )
9781, 96sseldd 3354 . . . . . . 7  |-  ( ph  ->  1  e.  R )
9888, 89clmsubcl 20616 . . . . . . 7  |-  ( ( H  e. CMod  /\  1  e.  R  /\  K  e.  R )  ->  (
1  -  K )  e.  R )
9980, 97, 94, 98syl3anc 1213 . . . . . 6  |-  ( ph  ->  ( 1  -  K
)  e.  R )
10088, 89cvsdivcl 20641 . . . . . 6  |-  ( ( H  e. CVec  /\  ( K  e.  R  /\  ( 1  -  K
)  e.  R  /\  ( 1  -  K
)  =/=  0 ) )  ->  ( K  /  ( 1  -  K ) )  e.  R )
10179, 94, 99, 25, 100syl13anc 1215 . . . . 5  |-  ( ph  ->  ( K  /  (
1  -  K ) )  e.  R )
102 clmgrp 20599 . . . . . . 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 15599 . . . . . 6  |-  ( ( H  e.  Grp  /\  Y  e.  P  /\  X  e.  P )  ->  ( Y  .-  X
)  e.  P )
109103, 104, 105, 108syl3anc 1213 . . . . 5  |-  ( ph  ->  ( Y  .-  X
)  e.  P )
110 ttgitvval.s . . . . . 6  |-  .x.  =  ( .s `  H )
111106, 88, 110, 89clmvsass 20618 . . . . 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 1215 . . . 4  |-  ( ph  ->  ( ( ( ( L  -  M )  /  M )  x.  ( K  /  (
1  -  K ) ) )  .x.  ( Y  .-  X ) )  =  ( ( ( L  -  M )  /  M )  .x.  ( ( K  / 
( 1  -  K
) )  .x.  ( Y  .-  X ) ) ) )
11346recnd 9408 . . . . . . 7  |-  ( ph  ->  ( L  -  M
)  e.  CC )
114113, 17, 19, 21, 22, 25divmuldivd 10144 . . . . . 6  |-  ( ph  ->  ( ( ( L  -  M )  /  M )  x.  ( K  /  ( 1  -  K ) ) )  =  ( ( ( L  -  M )  x.  K )  / 
( M  x.  (
1  -  K ) ) ) )
11555, 20oveq12d 6108 . . . . . 6  |-  ( ph  ->  ( ( ( L  -  M )  x.  K )  /  ( M  x.  ( 1  -  K ) ) )  =  ( ( ( L  x.  K
)  -  ( M  x.  K ) )  /  ( ( M  x.  1 )  -  ( M  x.  K
) ) ) )
116114, 115eqtrd 2473 . . . . 5  |-  ( ph  ->  ( ( ( L  -  M )  /  M )  x.  ( K  /  ( 1  -  K ) ) )  =  ( ( ( L  x.  K )  -  ( M  x.  K ) )  / 
( ( M  x.  1 )  -  ( M  x.  K )
) ) )
117116oveq1d 6105 . . . 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 15599 . . . . . . . 8  |-  ( ( H  e.  Grp  /\  X  e.  P  /\  A  e.  P )  ->  ( X  .-  A
)  e.  P )
120103, 105, 118, 119syl3anc 1213 . . . . . . 7  |-  ( ph  ->  ( X  .-  A
)  e.  P )
121 ttgcontlem1.y . . . . . . . . . 10  |-  ( ph  ->  ( X  .-  A
)  =  ( K 
.x.  ( Y  .-  A ) ) )
122121oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( X  .-  A ) )  =  ( ( 1  -  K )  .x.  ( K  .x.  ( Y 
.-  A ) ) ) )
12319, 21mulcomd 9403 . . . . . . . . . . 11  |-  ( ph  ->  ( K  x.  (
1  -  K ) )  =  ( ( 1  -  K )  x.  K ) )
124123oveq1d 6105 . . . . . . . . . 10  |-  ( ph  ->  ( ( K  x.  ( 1  -  K
) )  .x.  ( Y  .-  A ) )  =  ( ( ( 1  -  K )  x.  K )  .x.  ( Y  .-  A ) ) )
125106, 107grpsubcl 15599 . . . . . . . . . . . 12  |-  ( ( H  e.  Grp  /\  Y  e.  P  /\  A  e.  P )  ->  ( Y  .-  A
)  e.  P )
126103, 104, 118, 125syl3anc 1213 . . . . . . . . . . 11  |-  ( ph  ->  ( Y  .-  A
)  e.  P )
127106, 88, 110, 89clmvsass 20618 . . . . . . . . . . 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 1215 . . . . . . . . . 10  |-  ( ph  ->  ( ( K  x.  ( 1  -  K
) )  .x.  ( Y  .-  A ) )  =  ( K  .x.  ( ( 1  -  K )  .x.  ( Y  .-  A ) ) ) )
129106, 88, 110, 89clmvsass 20618 . . . . . . . . . . 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 1215 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 1  -  K )  x.  K )  .x.  ( Y  .-  A ) )  =  ( ( 1  -  K )  .x.  ( K  .x.  ( Y 
.-  A ) ) ) )
131124, 128, 1303eqtr3d 2481 . . . . . . . . 9  |-  ( ph  ->  ( K  .x.  (
( 1  -  K
)  .x.  ( Y  .-  A ) ) )  =  ( ( 1  -  K )  .x.  ( K  .x.  ( Y 
.-  A ) ) ) )
132 eqid 2441 . . . . . . . . . . . . 13  |-  ( -g `  (Scalar `  H )
)  =  ( -g `  (Scalar `  H )
)
133 clmlmod 20598 . . . . . . . . . . . . . 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 16983 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 (
-g `  (Scalar `  H
) ) K ) 
.x.  ( Y  .-  A ) )  =  ( ( 1  .x.  ( Y  .-  A
) )  .-  ( K  .x.  ( Y  .-  A ) ) ) )
13688, 89clmsub 20611 . . . . . . . . . . . . . 14  |-  ( ( H  e. CMod  /\  1  e.  R  /\  K  e.  R )  ->  (
1  -  K )  =  ( 1 (
-g `  (Scalar `  H
) ) K ) )
13780, 97, 94, 136syl3anc 1213 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  -  K
)  =  ( 1 ( -g `  (Scalar `  H ) ) K ) )
138137oveq1d 6105 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( Y  .-  A ) )  =  ( ( 1 ( -g `  (Scalar `  H ) ) K )  .x.  ( Y 
.-  A ) ) )
139106, 110clmvs1 20620 . . . . . . . . . . . . . . 15  |-  ( ( H  e. CMod  /\  ( Y  .-  A )  e.  P )  ->  (
1  .x.  ( Y  .-  A ) )  =  ( Y  .-  A
) )
14080, 126, 139syl2anc 656 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  .x.  ( Y  .-  A ) )  =  ( Y  .-  A ) )
141140eqcomd 2446 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y  .-  A
)  =  ( 1 
.x.  ( Y  .-  A ) ) )
142141, 121oveq12d 6108 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Y  .-  A )  .-  ( X  .-  A ) )  =  ( ( 1 
.x.  ( Y  .-  A ) )  .-  ( K  .x.  ( Y 
.-  A ) ) ) )
143135, 138, 1423eqtr4d 2483 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( Y  .-  A ) )  =  ( ( Y 
.-  A )  .-  ( X  .-  A ) ) )
144106, 107grpnnncan2 15614 . . . . . . . . . . . 12  |-  ( ( H  e.  Grp  /\  ( Y  e.  P  /\  X  e.  P  /\  A  e.  P
) )  ->  (
( Y  .-  A
)  .-  ( X  .-  A ) )  =  ( Y  .-  X
) )
145103, 104, 105, 118, 144syl13anc 1215 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Y  .-  A )  .-  ( X  .-  A ) )  =  ( Y  .-  X ) )
146143, 145eqtrd 2473 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  K )  .x.  ( Y  .-  A ) )  =  ( Y  .-  X ) )
147146oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( K  .x.  (
( 1  -  K
)  .x.  ( Y  .-  A ) ) )  =  ( K  .x.  ( Y  .-  X ) ) )
148122, 131, 1473eqtr2rd 2480 . . . . . . . 8  |-  ( ph  ->  ( K  .x.  ( Y  .-  X ) )  =  ( ( 1  -  K )  .x.  ( X  .-  A ) ) )
149106, 110, 88, 89, 79, 94, 99, 109, 120, 59, 148cvsmuleqdivd 20642 . . . . . . 7  |-  ( ph  ->  ( Y  .-  X
)  =  ( ( ( 1  -  K
)  /  K ) 
.x.  ( X  .-  A ) ) )
150106, 110, 88, 89, 79, 99, 94, 109, 120, 25, 59, 149cvsdiveqd 20643 . . . . . 6  |-  ( ph  ->  ( ( K  / 
( 1  -  K
) )  .x.  ( Y  .-  X ) )  =  ( X  .-  A ) )
151150, 120eqeltrd 2515 . . . . 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 15599 . . . . . . . . . 10  |-  ( ( H  e.  Grp  /\  N  e.  P  /\  A  e.  P )  ->  ( N  .-  A
)  e.  P )
155103, 153, 118, 154syl3anc 1213 . . . . . . . . 9  |-  ( ph  ->  ( N  .-  A
)  e.  P )
156106, 88, 110, 89lmodvscl 16945 . . . . . . . . 9  |-  ( ( H  e.  LMod  /\  L  e.  R  /\  ( N  .-  A )  e.  P )  ->  ( L  .x.  ( N  .-  A ) )  e.  P )
157134, 82, 155, 156syl3anc 1213 . . . . . . . 8  |-  ( ph  ->  ( L  .x.  ( N  .-  A ) )  e.  P )
158 ttgitvval.p . . . . . . . . 9  |-  .+  =  ( +g  `  H )
159106, 158grpcl 15544 . . . . . . . 8  |-  ( ( H  e.  Grp  /\  A  e.  P  /\  ( L  .x.  ( N 
.-  A ) )  e.  P )  -> 
( A  .+  ( L  .x.  ( N  .-  A ) ) )  e.  P )
160103, 118, 157, 159syl3anc 1213 . . . . . . 7  |-  ( ph  ->  ( A  .+  ( L  .x.  ( N  .-  A ) ) )  e.  P )
161152, 160eqeltrd 2515 . . . . . 6  |-  ( ph  ->  B  e.  P )
162106, 107grpsubcl 15599 . . . . . 6  |-  ( ( H  e.  Grp  /\  B  e.  P  /\  X  e.  P )  ->  ( B  .-  X
)  e.  P )
163103, 161, 105, 162syl3anc 1213 . . . . 5  |-  ( ph  ->  ( B  .-  X
)  e.  P )
164 ttgcontlem1.r . . . . . 6  |-  ( ph  ->  L  =/=  M )
16554, 17, 164subne0d 9724 . . . . 5  |-  ( ph  ->  ( L  -  M
)  =/=  0 )
166 ttgcontlem1.x . . . . . . . . . 10  |-  ( ph  ->  ( X  .-  A
)  =  ( M 
.x.  ( N  .-  A ) ) )
167166oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( ( L  -  M )  .x.  ( X  .-  A ) )  =  ( ( L  -  M )  .x.  ( M  .x.  ( N 
.-  A ) ) ) )
16817, 113mulcomd 9403 . . . . . . . . . . 11  |-  ( ph  ->  ( M  x.  ( L  -  M )
)  =  ( ( L  -  M )  x.  M ) )
169168oveq1d 6105 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  x.  ( L  -  M
) )  .x.  ( N  .-  A ) )  =  ( ( ( L  -  M )  x.  M )  .x.  ( N  .-  A ) ) )
170106, 88, 110, 89clmvsass 20618 . . . . . . . . . . 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 1215 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  x.  ( L  -  M
) )  .x.  ( N  .-  A ) )  =  ( M  .x.  ( ( L  -  M )  .x.  ( N  .-  A ) ) ) )
172106, 88, 110, 89clmvsass 20618 . . . . . . . . . . 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 1215 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  -  M )  x.  M )  .x.  ( N  .-  A ) )  =  ( ( L  -  M )  .x.  ( M  .x.  ( N 
.-  A ) ) ) )
174169, 171, 1733eqtr3d 2481 . . . . . . . . 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 16983 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L (
-g `  (Scalar `  H
) ) M ) 
.x.  ( N  .-  A ) )  =  ( ( L  .x.  ( N  .-  A ) )  .-  ( M 
.x.  ( N  .-  A ) ) ) )
17688, 89clmsub 20611 . . . . . . . . . . . . . 14  |-  ( ( H  e. CMod  /\  L  e.  R  /\  M  e.  R )  ->  ( L  -  M )  =  ( L (
-g `  (Scalar `  H
) ) M ) )
17780, 82, 87, 176syl3anc 1213 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  M
)  =  ( L ( -g `  (Scalar `  H ) ) M ) )
178177oveq1d 6105 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  -  M )  .x.  ( N  .-  A ) )  =  ( ( L ( -g `  (Scalar `  H ) ) M )  .x.  ( N 
.-  A ) ) )
179152oveq1d 6105 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  .-  A
)  =  ( ( A  .+  ( L 
.x.  ( N  .-  A ) ) ) 
.-  A ) )
180 lmodabl 16972 . . . . . . . . . . . . . . . 16  |-  ( H  e.  LMod  ->  H  e. 
Abel )
181134, 180syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H  e.  Abel )
182106, 158, 107ablpncan2 16298 . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  .+  ( L  .x.  ( N 
.-  A ) ) )  .-  A )  =  ( L  .x.  ( N  .-  A ) ) )
184179, 183eqtrd 2473 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  .-  A
)  =  ( L 
.x.  ( N  .-  A ) ) )
185184, 166oveq12d 6108 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  .-  A )  .-  ( X  .-  A ) )  =  ( ( L 
.x.  ( N  .-  A ) )  .-  ( M  .x.  ( N 
.-  A ) ) ) )
186175, 178, 1853eqtr4d 2483 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  -  M )  .x.  ( N  .-  A ) )  =  ( ( B 
.-  A )  .-  ( X  .-  A ) ) )
187106, 107grpnnncan2 15614 . . . . . . . . . . . 12  |-  ( ( H  e.  Grp  /\  ( B  e.  P  /\  X  e.  P  /\  A  e.  P
) )  ->  (
( B  .-  A
)  .-  ( X  .-  A ) )  =  ( B  .-  X
) )
188103, 161, 105, 118, 187syl13anc 1215 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  .-  A )  .-  ( X  .-  A ) )  =  ( B  .-  X ) )
189186, 188eqtrd 2473 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  -  M )  .x.  ( N  .-  A ) )  =  ( B  .-  X ) )
190189oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( M  .x.  (
( L  -  M
)  .x.  ( N  .-  A ) ) )  =  ( M  .x.  ( B  .-  X ) ) )
191167, 174, 1903eqtr2rd 2480 . . . . . . . 8  |-  ( ph  ->  ( M  .x.  ( B  .-  X ) )  =  ( ( L  -  M )  .x.  ( X  .-  A ) ) )
192106, 110, 88, 89, 79, 87, 91, 163, 120, 22, 191cvsmuleqdivd 20642 . . . . . . 7  |-  ( ph  ->  ( B  .-  X
)  =  ( ( ( L  -  M
)  /  M ) 
.x.  ( X  .-  A ) ) )
193106, 110, 88, 89, 79, 91, 87, 163, 120, 165, 22, 192cvsdiveqd 20643 . . . . . 6  |-  ( ph  ->  ( ( M  / 
( L  -  M
) )  .x.  ( B  .-  X ) )  =  ( X  .-  A ) )
194150, 193eqtr4d 2476 . . . . 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 20643 . . . 4  |-  ( ph  ->  ( ( ( L  -  M )  /  M )  .x.  (
( K  /  (
1  -  K ) )  .x.  ( Y 
.-  X ) ) )  =  ( B 
.-  X ) )
196112, 117, 1953eqtr3rd 2482 . . 3  |-  ( ph  ->  ( B  .-  X
)  =  ( ( ( ( L  x.  K )  -  ( M  x.  K )
)  /  ( ( M  x.  1 )  -  ( M  x.  K ) ) ) 
.x.  ( Y  .-  X ) ) )
197 oveq1 6097 . . . . 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 2452 . . . 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 3070 . . 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 656 . 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 23064 . 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 1364    e. wcel 1761    =/= wne 2604   E.wrex 2714    C_ wss 3325   class class class wbr 4289   ` cfv 5415  (class class class)co 6090   RRcr 9277   0cc0 9278   1c1 9279    x. cmul 9283   RR*cxr 9413    < clt 9414    <_ cle 9415    - cmin 9591    / cdiv 9989   RR+crp 10987   [,]cicc 11299   Basecbs 14170   +g cplusg 14234  Scalarcsca 14237   .scvsca 14238   Grpcgrp 15406   -gcsg 15409   Abelcabel 16271   LModclmod 16928  CModcclm 20593  CVecccvs 20635  Itvcitv 22856  toTGcttg 23054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-addf 9357  ax-mulf 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-tpos 6744  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-4 10378  df-5 10379  df-6 10380  df-7 10381  df-8 10382  df-9 10383  df-10 10384  df-n0 10576  df-z 10643  df-dec 10752  df-uz 10858  df-rp 10988  df-icc 11303  df-fz 11434  df-struct 14172  df-ndx 14173  df-slot 14174  df-base 14175  df-sets 14176  df-ress 14177  df-plusg 14247  df-mulr 14248  df-starv 14249  df-tset 14253  df-ple 14254  df-ds 14256  df-unif 14257  df-0g 14376  df-mnd 15411  df-grp 15538  df-minusg 15539  df-sbg 15540  df-subg 15671  df-cmn 16272  df-abl 16273  df-mgp 16582  df-ur 16594  df-rng 16637  df-cring 16638  df-oppr 16705  df-dvdsr 16723  df-unit 16724  df-invr 16754  df-dvr 16765  df-drng 16814  df-subrg 16843  df-lmod 16930  df-lvec 17162  df-cnfld 17778  df-clm 20594  df-cvs 20636  df-itv 22858  df-lng 22859  df-ttg 23055
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator