Metamath Proof Explorer

Theorem prlngmolem2

Description: Lemma for prlngmo . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses prlngeu.p 
|- P = ( Base ` G )
prlngeu.l 
|- L = ( LineG ` G )
prlngeu.r 
|- .|| = ( parlnG ` G )
prlngeu.g 
|- ( ph -> G e. TarskiG )
prlngeu.a 
|- ( ph -> A e. ran L )
prlngeu.x 
|- ( ph -> X e. ( P \ A ) )
prlngeu.1 
|- ( ph -> G e. TarskiGE )
prlngmolem2.1 
|- O = { <. x , y >. | ( ( x e. ( P \ b ) /\ y e. ( P \ b ) ) /\ E. r e. b r e. ( x ( Itv ` G ) y ) ) }
prlngmolem2.2 
|- Q = { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) }
Assertion prlngmolem2 
|- ( ph -> E* b e. ran L ( A .|| b /\ X e. b ) )

Proof

Step Hyp Ref Expression
1 prlngeu.p 
 |-  P = ( Base ` G )
2 prlngeu.l 
 |-  L = ( LineG ` G )
3 prlngeu.r 
 |-  .|| = ( parlnG ` G )
4 prlngeu.g 
 |-  ( ph -> G e. TarskiG )
5 prlngeu.a 
 |-  ( ph -> A e. ran L )
6 prlngeu.x 
 |-  ( ph -> X e. ( P \ A ) )
7 prlngeu.1 
 |-  ( ph -> G e. TarskiGE )
8 prlngmolem2.1 
 |-  O = { <. x , y >. | ( ( x e. ( P \ b ) /\ y e. ( P \ b ) ) /\ E. r e. b r e. ( x ( Itv ` G ) y ) ) }
9 prlngmolem2.2 
 |-  Q = { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) }
10 anass 
 |-  ( ( ( A .|| b /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) <-> ( A .|| b /\ ( X e. b /\ ( A .|| c /\ X e. c ) ) ) )
11 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) -> G e. TarskiG )
12 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) -> A e. ran L )
13 2 11 12 tglnne0 
 |-  ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) -> A =/= (/) )
14 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b = c ) -> b = c )
15 7 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> G e. TarskiGE )
16 11 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> G e. TarskiG )
17 16 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> G e. TarskiG )
18 12 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> A e. ran L )
19 6 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> X e. ( P \ A ) )
20 19 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> X e. ( P \ A ) )
21 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
22 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> b e. ran L )
23 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> b e. ran L )
24 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> c e. ran L )
25 24 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> c e. ran L )
26 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> A .|| b )
27 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> A .|| c )
28 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> X e. b )
29 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> X e. c )
30 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> X e. c )
31 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> t e. A )
32 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> w e. ( c \ b ) )
33 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> b =/= c )
34 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> w O t )
35 1 2 3 17 18 20 8 9 21 23 25 26 27 28 30 31 32 33 34 prlngmolem1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ w O t ) -> -. G e. TarskiGE )
36 16 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> G e. TarskiG )
37 12 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> A e. ran L )
38 19 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> X e. ( P \ A ) )
39 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> b e. ran L )
40 24 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> c e. ran L )
41 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> A .|| b )
42 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> A .|| c )
43 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> X e. b )
44 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> X e. c )
45 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> t e. A )
46 eqid 
 |-  ( dist ` G ) = ( dist ` G )
47 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
48 eqid 
 |-  ( ( pInvG ` G ) ` X ) = ( ( pInvG ` G ) ` X )
49 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( c \ b ) )
50 49 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. c )
51 50 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> w e. c )
52 1 46 21 2 47 36 48 40 44 51 mirln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> ( ( ( pInvG ` G ) ` X ) ` w ) e. c )
53 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> w e. ( c \ b ) )
54 53 eldifbd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> -. w e. b )
55 36 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> G e. TarskiG )
56 1 2 21 16 24 29 tglnpt 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> X e. P )
57 56 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> X e. P )
58 16 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> G e. TarskiG )
59 24 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> c e. ran L )
60 1 2 21 58 59 50 tglnpt 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. P )
61 60 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> w e. P )
62 1 46 21 2 47 55 57 48 61 mirmir 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> ( ( ( pInvG ` G ) ` X ) ` ( ( ( pInvG ` G ) ` X ) ` w ) ) = w )
63 39 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> b e. ran L )
64 43 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> X e. b )
65 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> ( ( ( pInvG ` G ) ` X ) ` w ) e. b )
66 1 46 21 2 47 55 48 63 64 65 mirln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> ( ( ( pInvG ` G ) ` X ) ` ( ( ( pInvG ` G ) ` X ) ` w ) ) e. b )
67 62 66 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) e. b ) -> w e. b )
68 54 67 mtand 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> -. ( ( ( pInvG ` G ) ` X ) ` w ) e. b )
69 52 68 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> ( ( ( pInvG ` G ) ` X ) ` w ) e. ( c \ b ) )
70 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> b =/= c )
71 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> ( ( ( pInvG ` G ) ` X ) ` w ) O t )
72 1 2 3 36 37 38 8 9 21 39 40 41 42 43 44 45 69 70 71 prlngmolem1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) -> -. G e. TarskiGE )
73 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
74 22 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> b e. ran L )
75 49 eldifbd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> -. w e. b )
76 60 75 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( P \ b ) )
77 12 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A e. ran L )
78 6 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> X e. ( P \ A ) )
79 1 21 2 73 58 77 78 elplnglnid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A C_ ( A ( PlnG ` G ) X ) )
80 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. A )
81 79 80 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( A ( PlnG ` G ) X ) )
82 1 2 73 58 77 78 tgelrnpln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A ( PlnG ` G ) X ) e. ran ( PlnG ` G ) )
83 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A .|| c )
84 29 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> X e. c )
85 6 eldifbd 
 |-  ( ph -> -. X e. A )
86 85 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> -. X e. A )
87 nelne1 
 |-  ( ( X e. c /\ -. X e. A ) -> c =/= A )
88 84 86 87 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> c =/= A )
89 88 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A =/= c )
90 2 73 3 58 83 89 50 84 prlnghpg 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w ( ( hpG ` G ) ` A ) X )
91 1 2 73 77 60 78 58 90 hpgssplng 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( A ( PlnG ` G ) X ) )
92 91 75 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( ( A ( PlnG ` G ) X ) \ b ) )
93 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A .|| b )
94 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> X e. b )
95 nelne1 
 |-  ( ( X e. b /\ -. X e. A ) -> b =/= A )
96 94 86 95 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> b =/= A )
97 96 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A =/= b )
98 2 73 3 58 93 97 94 prlngpln3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> b C_ ( A ( PlnG ` G ) X ) )
99 1 2 73 58 82 74 92 98 plng3p 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A ( PlnG ` G ) X ) = ( b ( PlnG ` G ) w ) )
100 81 99 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( b ( PlnG ` G ) w ) )
101 2 3 58 93 97 prlngin0 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A i^i b ) = (/) )
102 101 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ t e. b ) -> ( A i^i b ) = (/) )
103 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ t e. b ) -> t e. A )
104 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ t e. b ) -> t e. b )
105 103 104 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ t e. b ) -> t e. ( A i^i b ) )
106 105 ne0d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ t e. b ) -> ( A i^i b ) =/= (/) )
107 106 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) /\ t e. b ) -> -. ( A i^i b ) = (/) )
108 102 107 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> -. t e. b )
109 100 108 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( ( b ( PlnG ` G ) w ) \ b ) )
110 1 21 2 73 47 48 8 58 74 76 109 94 plngmiropp 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( w O t \/ ( ( ( pInvG ` G ) ` X ) ` w ) O t ) )
111 35 72 110 mpjaodan 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> -. G e. TarskiGE )
112 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> b =/= c )
113 112 necomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> c =/= b )
114 1 21 2 16 24 22 29 113 tglnpt4 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> E. w e. ( c \ b ) w =/= X )
115 111 114 r19.29a 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> -. G e. TarskiGE )
116 15 115 pm2.21dd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) -> b = c )
117 14 116 pm2.61dane 
 |-  ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) /\ t e. A ) -> b = c )
118 13 117 n0limd 
 |-  ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ A .|| c ) /\ X e. c ) -> b = c )
119 118 anasss 
 |-  ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) -> b = c )
120 119 anasss 
 |-  ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .|| b ) /\ ( X e. b /\ ( A .|| c /\ X e. c ) ) ) -> b = c )
121 120 anasss 
 |-  ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ ( A .|| b /\ ( X e. b /\ ( A .|| c /\ X e. c ) ) ) ) -> b = c )
122 10 121 sylan2b 
 |-  ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ ( ( A .|| b /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) ) -> b = c )
123 122 ex 
 |-  ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) -> ( ( ( A .|| b /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) -> b = c ) )
124 123 ralrimiva 
 |-  ( ( ph /\ b e. ran L ) -> A. c e. ran L ( ( ( A .|| b /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) -> b = c ) )
125 124 ralrimiva 
 |-  ( ph -> A. b e. ran L A. c e. ran L ( ( ( A .|| b /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) -> b = c ) )
126 breq2 
 |-  ( b = c -> ( A .|| b <-> A .|| c ) )
127 eleq2w 
 |-  ( b = c -> ( X e. b <-> X e. c ) )
128 126 127 anbi12d 
 |-  ( b = c -> ( ( A .|| b /\ X e. b ) <-> ( A .|| c /\ X e. c ) ) )
129 128 rmo4 
 |-  ( E* b e. ran L ( A .|| b /\ X e. b ) <-> A. b e. ran L A. c e. ran L ( ( ( A .|| b /\ X e. b ) /\ ( A .|| c /\ X e. c ) ) -> b = c ) )
130 125 129 sylibr 
 |-  ( ph -> E* b e. ran L ( A .|| b /\ X e. b ) )