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

Theorem colperpexlem3 23926
Description: Lemma for colperpex 23927. Case 1 of theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p  |-  P  =  ( Base `  G
)
colperpex.d  |-  .-  =  ( dist `  G )
colperpex.i  |-  I  =  (Itv `  G )
colperpex.l  |-  L  =  (LineG `  G )
colperpex.g  |-  ( ph  ->  G  e. TarskiG )
colperpex.1  |-  ( ph  ->  A  e.  P )
colperpex.2  |-  ( ph  ->  B  e.  P )
colperpex.3  |-  ( ph  ->  C  e.  P )
colperpex.4  |-  ( ph  ->  A  =/=  B )
colperpexlem3.1  |-  ( ph  ->  -.  C  e.  ( A L B ) )
Assertion
Ref Expression
colperpexlem3  |-  ( ph  ->  E. p  e.  P  ( ( A L p ) (⟂G `  G
) ( A L B )  /\  E. t  e.  P  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
Distinct variable groups:    .- , p, t    A, p, t    B, p, t    C, p, t    G, p, t    I, p, t    L, p, t    P, p, t    ph, p, t

Proof of Theorem colperpexlem3
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 colperpex.p . . . 4  |-  P  =  ( Base `  G
)
2 colperpex.d . . . 4  |-  .-  =  ( dist `  G )
3 colperpex.i . . . 4  |-  I  =  (Itv `  G )
4 colperpex.l . . . 4  |-  L  =  (LineG `  G )
5 eqid 2467 . . . 4  |-  (pInvG `  G )  =  (pInvG `  G )
6 colperpex.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
76ad2antrr 725 . . . 4  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  G  e. TarskiG )
8 eqid 2467 . . . 4  |-  ( (pInvG `  G ) `  p
)  =  ( (pInvG `  G ) `  p
)
9 colperpex.1 . . . . . . . 8  |-  ( ph  ->  A  e.  P )
10 colperpex.2 . . . . . . . 8  |-  ( ph  ->  B  e.  P )
11 colperpex.4 . . . . . . . 8  |-  ( ph  ->  A  =/=  B )
121, 3, 4, 6, 9, 10, 11tgelrnln 23839 . . . . . . 7  |-  ( ph  ->  ( A L B )  e.  ran  L
)
1312ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A L B )  e.  ran  L )
14 simplr 754 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  x  e.  ( A L B ) )
151, 4, 3, 7, 13, 14tglnpt 23779 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  x  e.  P
)
16 eqid 2467 . . . . 5  |-  ( (pInvG `  G ) `  x
)  =  ( (pInvG `  G ) `  x
)
17 colperpex.3 . . . . . 6  |-  ( ph  ->  C  e.  P )
1817ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  C  e.  P
)
191, 2, 3, 4, 5, 7, 15, 16, 18mircl 23870 . . . 4  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( ( (pInvG `  G ) `  x
) `  C )  e.  P )
209ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  A  e.  P
)
21 eqid 2467 . . . . 5  |-  ( (pInvG `  G ) `  A
)  =  ( (pInvG `  G ) `  A
)
221, 2, 3, 4, 5, 7, 20, 21, 18mircl 23870 . . . 4  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( ( (pInvG `  G ) `  A
) `  C )  e.  P )
231, 2, 3, 4, 5, 7, 20, 21, 18mircgr 23866 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A  .-  ( ( (pInvG `  G ) `  A
) `  C )
)  =  ( A 
.-  C ) )
2410ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  B  e.  P
)
25 colperpexlem3.1 . . . . . . . . . . . 12  |-  ( ph  ->  -.  C  e.  ( A L B ) )
2625ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  -.  C  e.  ( A L B ) )
27 nelne2 2797 . . . . . . . . . . 11  |-  ( ( x  e.  ( A L B )  /\  -.  C  e.  ( A L B ) )  ->  x  =/=  C
)
2814, 26, 27syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  x  =/=  C
)
291, 3, 4, 7, 15, 18, 28tglinecom 23844 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( x L C )  =  ( C L x ) )
3028necomd 2738 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  C  =/=  x
)
311, 3, 4, 7, 18, 15, 30tgelrnln 23839 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( C L x )  e.  ran  L )
3229, 31eqeltrd 2555 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( x L C )  e.  ran  L )
33 simpr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( C L x ) (⟂G `  G
) ( A L B ) )
3429, 33eqbrtrd 4472 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( x L C ) (⟂G `  G
) ( A L B ) )
351, 2, 3, 4, 7, 32, 13, 34perpcom 23913 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A L B ) (⟂G `  G
) ( x L C ) )
361, 2, 3, 4, 7, 20, 24, 14, 18, 35perprag 23920 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  <" A x C ">  e.  (∟G `  G ) )
371, 2, 3, 4, 5, 7, 20, 15, 18israg 23897 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( <" A x C ">  e.  (∟G `  G )  <->  ( A  .-  C )  =  ( A  .-  ( ( (pInvG `  G ) `  x ) `  C
) ) ) )
3836, 37mpbid 210 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A  .-  C )  =  ( A  .-  ( ( (pInvG `  G ) `  x ) `  C
) ) )
3923, 38eqtr2d 2509 . . . 4  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A  .-  ( ( (pInvG `  G ) `  x
) `  C )
)  =  ( A 
.-  ( ( (pInvG `  G ) `  A
) `  C )
) )
401, 2, 3, 4, 5, 7, 8, 19, 22, 20, 39midexlem 23892 . . 3  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  E. p  e.  P  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )
417ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  G  e. TarskiG )
4222ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( (pInvG `  G ) `  A
) `  C )  e.  P )
4320ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  A  e.  P )
4418ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  C  e.  P )
4519ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( (pInvG `  G ) `  x
) `  C )  e.  P )
4615ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  x  e.  P )
47 simplr 754 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  p  e.  P )
481, 2, 3, 4, 5, 41, 43, 21, 44mirbtwn 23867 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  A  e.  ( (
( (pInvG `  G
) `  A ) `  C ) I C ) )
491, 2, 3, 4, 5, 41, 46, 16, 44mirbtwn 23867 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  x  e.  ( (
( (pInvG `  G
) `  x ) `  C ) I C ) )
501, 2, 3, 4, 5, 41, 47, 8, 45mirbtwn 23867 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  p  e.  ( (
( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) I ( ( (pInvG `  G ) `  x ) `  C
) ) )
51 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )
5251eqcomd 2475 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) )  =  ( ( (pInvG `  G
) `  A ) `  C ) )
5352oveq1d 6309 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) I ( ( (pInvG `  G
) `  x ) `  C ) )  =  ( ( ( (pInvG `  G ) `  A
) `  C )
I ( ( (pInvG `  G ) `  x
) `  C )
) )
5450, 53eleqtrd 2557 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  p  e.  ( (
( (pInvG `  G
) `  A ) `  C ) I ( ( (pInvG `  G
) `  x ) `  C ) ) )
551, 2, 3, 41, 42, 43, 44, 45, 46, 47, 48, 49, 54tgtrisegint 23733 . . . . . . 7  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  E. t  e.  P  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )
5641ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  G  e. TarskiG )
5743ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  A  e.  P )
58 simpllr 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  e.  P )
59 simplrr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  e.  ( A I x ) )
60 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  x  =  A )
6160oveq2d 6310 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  ( A I x )  =  ( A I A ) )
6259, 61eleqtrd 2557 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  e.  ( A I A ) )
631, 2, 3, 56, 57, 58, 62axtgbtwnid 23706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  A  =  t )
6463eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  =  A )
6564oveq1d 6309 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
t L p )  =  ( A L p ) )
6652ad3antrrr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
)  =  ( ( (pInvG `  G ) `  A ) `  C
) )
6760fveq2d 5875 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
(pInvG `  G ) `  x )  =  ( (pInvG `  G ) `  A ) )
6867fveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( (pInvG `  G
) `  x ) `  C )  =  ( ( (pInvG `  G
) `  A ) `  C ) )
6966, 68eqtr4d 2511 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
)  =  ( ( (pInvG `  G ) `  x ) `  C
) )
7047ad3antrrr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  p  e.  P )
7145ad3antrrr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( (pInvG `  G
) `  x ) `  C )  e.  P
)
721, 2, 3, 4, 5, 56, 70, 8, 71mirinv 23875 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) )  =  ( ( (pInvG `  G
) `  x ) `  C )  <->  p  =  ( ( (pInvG `  G ) `  x
) `  C )
) )
7369, 72mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  p  =  ( ( (pInvG `  G ) `  x
) `  C )
)
7446ad3antrrr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  x  e.  P )
7560oveq1d 6309 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
x I x )  =  ( A I x ) )
7659, 75eleqtrrd 2558 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  e.  ( x I x ) )
771, 2, 3, 56, 74, 58, 76axtgbtwnid 23706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  x  =  t )
7877eqcomd 2475 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  =  x )
7973, 78oveq12d 6312 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
p L t )  =  ( ( ( (pInvG `  G ) `  x ) `  C
) L x ) )
8036ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  <" A x C ">  e.  (∟G `  G ) )
811, 2, 3, 4, 5, 41, 47, 8, 45, 52mircom 23872 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  A ) `  C
) )  =  ( ( (pInvG `  G
) `  x ) `  C ) )
8228ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  x  =/=  C )
831, 2, 3, 4, 41, 5, 21, 16, 8, 43, 46, 44, 47, 80, 81, 82colperpexlem2 23925 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  A  =/=  p )
8483ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  A  =/=  p )
8564, 84eqnetrd 2760 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  =/=  p )
861, 3, 4, 56, 58, 70, 85tglinecom 23844 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
t L p )  =  ( p L t ) )
8744ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  C  e.  P )
8882ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  x  =/=  C )
8956adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  G  e. TarskiG )
9074adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  x  e.  P )
9187adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  C  e.  P )
921, 2, 3, 4, 5, 89, 90, 16mircinv 23876 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  ( (
(pInvG `  G ) `  x ) `  x
)  =  x )
93 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  ( (
(pInvG `  G ) `  x ) `  C
)  =  x )
9492, 93eqtr4d 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  ( (
(pInvG `  G ) `  x ) `  x
)  =  ( ( (pInvG `  G ) `  x ) `  C
) )
951, 2, 3, 4, 5, 89, 90, 16, 90, 91, 94mireq 23874 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  x  =  C )
9688adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  x  =/=  C )
9796neneqd 2669 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  /\  t  e.  P )  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  /\  (
( (pInvG `  G
) `  x ) `  C )  =  x )  ->  -.  x  =  C )
9895, 97pm2.65da 576 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  -.  ( ( (pInvG `  G ) `  x
) `  C )  =  x )
9998neqned 2670 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( (pInvG `  G
) `  x ) `  C )  =/=  x
)
10049ad3antrrr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  x  e.  ( ( ( (pInvG `  G ) `  x
) `  C )
I C ) )
1011, 3, 4, 56, 74, 87, 71, 88, 100btwnlng2 23829 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( (pInvG `  G
) `  x ) `  C )  e.  ( x L C ) )
1021, 3, 4, 56, 74, 87, 88, 71, 99, 101tglineelsb2 23841 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
x L C )  =  ( x L ( ( (pInvG `  G ) `  x
) `  C )
) )
10330ad5antr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  C  =/=  x )
1041, 3, 4, 56, 87, 74, 103tglinecom 23844 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  ( C L x )  =  ( x L C ) )
1051, 3, 4, 56, 71, 74, 99tglinecom 23844 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
( ( (pInvG `  G ) `  x
) `  C ) L x )  =  ( x L ( ( (pInvG `  G
) `  x ) `  C ) ) )
106102, 104, 1053eqtr4d 2518 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  ( C L x )  =  ( ( ( (pInvG `  G ) `  x
) `  C ) L x ) )
10779, 86, 1063eqtr4d 2518 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
t L p )  =  ( C L x ) )
10865, 107eqtr3d 2510 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  ( A L p )  =  ( C L x ) )
10933ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  ( C L x ) (⟂G `  G ) ( A L B ) )
110108, 109eqbrtrd 4472 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  ( A L p ) (⟂G `  G ) ( A L B ) )
11141ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  G  e. TarskiG )
11243ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  e.  P )
11347ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  p  e.  P )
11483ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  =/=  p )
1151, 3, 4, 111, 112, 113, 114tgelrnln 23839 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  ( A L p )  e. 
ran  L )
11613ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  ( A L B )  e. 
ran  L )
1171, 3, 4, 111, 112, 113, 114tglinerflx1 23842 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  e.  ( A L p ) )
11811ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  A  =/=  B
)
1191, 3, 4, 7, 20, 24, 118tglinerflx1 23842 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  A  e.  ( A L B ) )
120119ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  e.  ( A L B ) )
121117, 120elind 3693 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  e.  ( ( A L p )  i^i  ( A L B ) ) )
1221, 3, 4, 111, 112, 113, 114tglinerflx2 23843 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  p  e.  ( A L p ) )
12314ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  x  e.  ( A L B ) )
124114necomd 2738 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  p  =/=  A )
125 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  x  =/=  A )
12646ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  x  e.  P )
1271, 2, 3, 4, 41, 5, 21, 16, 8, 43, 46, 44, 47, 80, 81colperpexlem1 23924 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  <" x A p ">  e.  (∟G `  G ) )
128127ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  <" x A p ">  e.  (∟G `  G )
)
1291, 2, 3, 4, 5, 111, 126, 112, 113, 128ragcom 23898 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  <" p A x ">  e.  (∟G `  G )
)
1301, 2, 3, 4, 111, 115, 116, 121, 122, 123, 124, 125, 129ragperp 23917 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  ( A L p ) (⟂G `  G ) ( A L B ) )
131110, 130pm2.61dane 2785 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  -> 
( A L p ) (⟂G `  G
) ( A L B ) )
132119ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  A  e.  ( A L B ) )
13364, 132eqeltrd 2555 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  t  e.  ( A L B ) )
134133orcd 392 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =  A )  ->  (
t  e.  ( A L B )  \/  A  =  B ) )
13524ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  B  e.  P )
136118ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  =/=  B )
137 simpllr 758 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  t  e.  P )
138125necomd 2738 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  A  =/=  x )
139 simplrr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  t  e.  ( A I x ) )
1401, 3, 4, 111, 112, 126, 137, 138, 139btwnlng1 23828 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  t  e.  ( A L x ) )
1411, 3, 4, 111, 112, 135, 136, 126, 125, 123, 137, 140tglineeltr 23840 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  t  e.  ( A L B ) )
142141orcd 392 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  /\  (
( (pInvG `  G
) `  A ) `  C )  =  ( ( (pInvG `  G
) `  p ) `  ( ( (pInvG `  G ) `  x
) `  C )
) )  /\  t  e.  P )  /\  (
t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  /\  x  =/= 
A )  ->  (
t  e.  ( A L B )  \/  A  =  B ) )
143134, 142pm2.61dane 2785 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  -> 
( t  e.  ( A L B )  \/  A  =  B ) )
14441ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  ->  G  e. TarskiG )
14547ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  ->  p  e.  P )
146 simplr 754 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  -> 
t  e.  P )
14744ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  ->  C  e.  P )
148 simprl 755 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  -> 
t  e.  ( p I C ) )
1491, 2, 3, 144, 145, 146, 147, 148tgbtwncom 23722 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  -> 
t  e.  ( C I p ) )
150131, 143, 149jca32 535 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  /\  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) ) )  -> 
( ( A L p ) (⟂G `  G
) ( A L B )  /\  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
151150ex 434 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  p  e.  P
)  /\  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) ) )  /\  t  e.  P
)  ->  ( (
t  e.  ( p I C )  /\  t  e.  ( A I x ) )  ->  ( ( A L p ) (⟂G `  G ) ( A L B )  /\  ( ( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) ) )
152151reximdva 2942 . . . . . . 7  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( E. t  e.  P  ( t  e.  ( p I C )  /\  t  e.  ( A I x ) )  ->  E. t  e.  P  ( ( A L p ) (⟂G `  G ) ( A L B )  /\  ( ( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) ) )
15355, 152mpd 15 . . . . . 6  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  ->  E. t  e.  P  ( ( A L p ) (⟂G `  G
) ( A L B )  /\  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
154 r19.42v 3021 . . . . . 6  |-  ( E. t  e.  P  ( ( A L p ) (⟂G `  G
) ( A L B )  /\  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) )  <->  ( ( A L p ) (⟂G `  G ) ( A L B )  /\  E. t  e.  P  ( ( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
155153, 154sylib 196 . . . . 5  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  p  e.  P )  /\  ( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) ) )  -> 
( ( A L p ) (⟂G `  G
) ( A L B )  /\  E. t  e.  P  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
156155ex 434 . . . 4  |-  ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  p  e.  P )  ->  (
( ( (pInvG `  G ) `  A
) `  C )  =  ( ( (pInvG `  G ) `  p
) `  ( (
(pInvG `  G ) `  x ) `  C
) )  ->  (
( A L p ) (⟂G `  G
) ( A L B )  /\  E. t  e.  P  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) ) )
157156reximdva 2942 . . 3  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( E. p  e.  P  ( (
(pInvG `  G ) `  A ) `  C
)  =  ( ( (pInvG `  G ) `  p ) `  (
( (pInvG `  G
) `  x ) `  C ) )  ->  E. p  e.  P  ( ( A L p ) (⟂G `  G
) ( A L B )  /\  E. t  e.  P  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) ) )
15840, 157mpd 15 . 2  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  E. p  e.  P  ( ( A L p ) (⟂G `  G
) ( A L B )  /\  E. t  e.  P  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
1591, 2, 3, 4, 6, 12, 17, 25footex 23918 . 2  |-  ( ph  ->  E. x  e.  ( A L B ) ( C L x ) (⟂G `  G
) ( A L B ) )
160158, 159r19.29a 3008 1  |-  ( ph  ->  E. p  e.  P  ( ( A L p ) (⟂G `  G
) ( A L B )  /\  E. t  e.  P  (
( t  e.  ( A L B )  \/  A  =  B )  /\  t  e.  ( C I p ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369    = wceq 1379    e. wcel 1767    =/= wne 2662   E.wrex 2818   class class class wbr 4452   ran crn 5005   ` cfv 5593  (class class class)co 6294   <"cs3 12782   Basecbs 14502   distcds 14576  TarskiGcstrkg 23668  Itvcitv 23675  LineGclng 23676  pInvGcmir 23861  ∟Gcrag 23893  ⟂Gcperpg 23895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6586  ax-cnex 9558  ax-resscn 9559  ax-1cn 9560  ax-icn 9561  ax-addcl 9562  ax-addrcl 9563  ax-mulcl 9564  ax-mulrcl 9565  ax-mulcom 9566  ax-addass 9567  ax-mulass 9568  ax-distr 9569  ax-i2m1 9570  ax-1ne0 9571  ax-1rid 9572  ax-rnegex 9573  ax-rrecex 9574  ax-cnre 9575  ax-pre-lttri 9576  ax-pre-lttrn 9577  ax-pre-ltadd 9578  ax-pre-mulgt0 9579
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4251  df-int 4288  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6255  df-ov 6297  df-oprab 6298  df-mpt2 6299  df-om 6695  df-1st 6794  df-2nd 6795  df-recs 7052  df-rdg 7086  df-1o 7140  df-oadd 7144  df-er 7321  df-map 7432  df-pm 7433  df-en 7527  df-dom 7528  df-sdom 7529  df-fin 7530  df-card 8330  df-cda 8558  df-pnf 9640  df-mnf 9641  df-xr 9642  df-ltxr 9643  df-le 9644  df-sub 9817  df-neg 9818  df-nn 10547  df-2 10604  df-3 10605  df-n0 10806  df-z 10875  df-uz 11093  df-fz 11683  df-fzo 11803  df-hash 12384  df-word 12518  df-concat 12520  df-s1 12521  df-s2 12788  df-s3 12789  df-trkgc 23687  df-trkgb 23688  df-trkgcb 23689  df-trkg 23693  df-cgrg 23746  df-leg 23812  df-mir 23862  df-rag 23894  df-perpg 23896
This theorem is referenced by:  colperpex  23927
  Copyright terms: Public domain W3C validator