Metamath Proof Explorer

Theorem prlnghpg

Description: If two lines A and B are parallel, then any two points X and Y of B lie on the same half-plane limited by A . Theorem 12.6 of Schwabhauser p. 122. . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses prlnghpg.l 
|- L = ( LineG ` G )
prlnghpg.e 
|- E = ( PlnG ` G )
prlnghpg.p 
|- .|| = ( parlnG ` G )
prlnghpg.g 
|- ( ph -> G e. TarskiG )
prlnghpg.1 
|- ( ph -> A .|| B )
prlnghpg.2 
|- ( ph -> A =/= B )
prlnghpg.x 
|- ( ph -> X e. B )
prlnghpg.y 
|- ( ph -> Y e. B )
Assertion prlnghpg 
|- ( ph -> X ( ( hpG ` G ) ` A ) Y )

Proof

Step Hyp Ref Expression
1 prlnghpg.l 
 |-  L = ( LineG ` G )
2 prlnghpg.e 
 |-  E = ( PlnG ` G )
3 prlnghpg.p 
 |-  .|| = ( parlnG ` G )
4 prlnghpg.g 
 |-  ( ph -> G e. TarskiG )
5 prlnghpg.1 
 |-  ( ph -> A .|| B )
6 prlnghpg.2 
 |-  ( ph -> A =/= B )
7 prlnghpg.x 
 |-  ( ph -> X e. B )
8 prlnghpg.y 
 |-  ( ph -> Y e. B )
9 eqid 
 |-  ( Base ` G ) = ( Base ` G )
10 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
11 1 2 3 4 brprlng 
 |-  ( ph -> ( A .|| B <-> ( ( A e. ran L /\ B e. ran L ) /\ ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) ) )
12 5 11 mpbid 
 |-  ( ph -> ( ( A e. ran L /\ B e. ran L ) /\ ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) )
13 12 simpld 
 |-  ( ph -> ( A e. ran L /\ B e. ran L ) )
14 13 simpld 
 |-  ( ph -> A e. ran L )
15 13 simprd 
 |-  ( ph -> B e. ran L )
16 9 1 10 4 15 8 tglnpt 
 |-  ( ph -> Y e. ( Base ` G ) )
17 eleq1w 
 |-  ( a = c -> ( a e. ( ( Base ` G ) \ A ) <-> c e. ( ( Base ` G ) \ A ) ) )
18 eleq1w 
 |-  ( b = d -> ( b e. ( ( Base ` G ) \ A ) <-> d e. ( ( Base ` G ) \ A ) ) )
19 17 18 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) <-> ( c e. ( ( Base ` G ) \ A ) /\ d e. ( ( Base ` G ) \ A ) ) ) )
20 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a ( Itv ` G ) b ) = ( c ( Itv ` G ) d ) )
21 20 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( s e. ( a ( Itv ` G ) b ) <-> s e. ( c ( Itv ` G ) d ) ) )
22 21 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. A s e. ( a ( Itv ` G ) b ) <-> E. s e. A s e. ( c ( Itv ` G ) d ) ) )
23 eleq1w 
 |-  ( s = t -> ( s e. ( c ( Itv ` G ) d ) <-> t e. ( c ( Itv ` G ) d ) ) )
24 23 cbvrexvw 
 |-  ( E. s e. A s e. ( c ( Itv ` G ) d ) <-> E. t e. A t e. ( c ( Itv ` G ) d ) )
25 22 24 bitrdi 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. A s e. ( a ( Itv ` G ) b ) <-> E. t e. A t e. ( c ( Itv ` G ) d ) ) )
26 19 25 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) <-> ( ( c e. ( ( Base ` G ) \ A ) /\ d e. ( ( Base ` G ) \ A ) ) /\ E. t e. A t e. ( c ( Itv ` G ) d ) ) ) )
27 26 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } = { <. c , d >. | ( ( c e. ( ( Base ` G ) \ A ) /\ d e. ( ( Base ` G ) \ A ) ) /\ E. t e. A t e. ( c ( Itv ` G ) d ) ) }
28 9 1 10 4 15 7 tglnpt 
 |-  ( ph -> X e. ( Base ` G ) )
29 4 adantr 
 |-  ( ( ph /\ Y = X ) -> G e. TarskiG )
30 14 adantr 
 |-  ( ( ph /\ Y = X ) -> A e. ran L )
31 16 adantr 
 |-  ( ( ph /\ Y = X ) -> Y e. ( Base ` G ) )
32 12 simprd 
 |-  ( ph -> ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) )
33 6 neneqd 
 |-  ( ph -> -. A = B )
34 32 33 orcnd 
 |-  ( ph -> ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) )
35 34 simprd 
 |-  ( ph -> ( A i^i B ) = (/) )
36 35 adantr 
 |-  ( ( ph /\ Y e. A ) -> ( A i^i B ) = (/) )
37 simpr 
 |-  ( ( ph /\ Y e. A ) -> Y e. A )
38 8 adantr 
 |-  ( ( ph /\ Y e. A ) -> Y e. B )
39 inelcm 
 |-  ( ( Y e. A /\ Y e. B ) -> ( A i^i B ) =/= (/) )
40 37 38 39 syl2anc 
 |-  ( ( ph /\ Y e. A ) -> ( A i^i B ) =/= (/) )
41 40 neneqd 
 |-  ( ( ph /\ Y e. A ) -> -. ( A i^i B ) = (/) )
42 36 41 pm2.65da 
 |-  ( ph -> -. Y e. A )
43 42 adantr 
 |-  ( ( ph /\ Y = X ) -> -. Y e. A )
44 9 10 1 29 30 31 27 43 hpgid 
 |-  ( ( ph /\ Y = X ) -> Y ( ( hpG ` G ) ` A ) Y )
45 simpr 
 |-  ( ( ph /\ Y = X ) -> Y = X )
46 44 45 breqtrd 
 |-  ( ( ph /\ Y = X ) -> Y ( ( hpG ` G ) ` A ) X )
47 42 adantr 
 |-  ( ( ph /\ Y =/= X ) -> -. Y e. A )
48 35 ad2antrr 
 |-  ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) -> ( A i^i B ) = (/) )
49 simplr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> t e. A )
50 4 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> G e. TarskiG )
51 16 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> Y e. ( Base ` G ) )
52 28 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> X e. ( Base ` G ) )
53 14 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> A e. ran L )
54 9 1 10 50 53 49 tglnpt 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> t e. ( Base ` G ) )
55 simp-4r 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> Y =/= X )
56 simpr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> t e. ( Y ( Itv ` G ) X ) )
57 9 10 1 50 51 52 54 55 56 btwnlng1 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> t e. ( Y L X ) )
58 15 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> B e. ran L )
59 8 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> Y e. B )
60 7 ad4antr 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> X e. B )
61 9 10 1 50 51 52 55 55 58 59 60 tglinethru 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> B = ( Y L X ) )
62 57 61 eleqtrrd 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> t e. B )
63 inelcm 
 |-  ( ( t e. A /\ t e. B ) -> ( A i^i B ) =/= (/) )
64 49 62 63 syl2anc 
 |-  ( ( ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) /\ t e. A ) /\ t e. ( Y ( Itv ` G ) X ) ) -> ( A i^i B ) =/= (/) )
65 eqid 
 |-  ( dist ` G ) = ( dist ` G )
66 9 65 10 27 16 28 islnopp 
 |-  ( ph -> ( Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X <-> ( ( -. Y e. A /\ -. X e. A ) /\ E. t e. A t e. ( Y ( Itv ` G ) X ) ) ) )
67 66 adantr 
 |-  ( ( ph /\ Y =/= X ) -> ( Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X <-> ( ( -. Y e. A /\ -. X e. A ) /\ E. t e. A t e. ( Y ( Itv ` G ) X ) ) ) )
68 67 simplbda 
 |-  ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) -> E. t e. A t e. ( Y ( Itv ` G ) X ) )
69 64 68 r19.29a 
 |-  ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) -> ( A i^i B ) =/= (/) )
70 69 neneqd 
 |-  ( ( ( ph /\ Y =/= X ) /\ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) -> -. ( A i^i B ) = (/) )
71 48 70 pm2.65da 
 |-  ( ( ph /\ Y =/= X ) -> -. Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X )
72 simpr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> B C_ h )
73 4 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> G e. TarskiG )
74 simpllr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> h e. ran E )
75 14 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> A e. ran L )
76 7 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> X e. B )
77 72 76 sseldd 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> X e. h )
78 35 adantr 
 |-  ( ( ph /\ X e. A ) -> ( A i^i B ) = (/) )
79 simpr 
 |-  ( ( ph /\ X e. A ) -> X e. A )
80 7 adantr 
 |-  ( ( ph /\ X e. A ) -> X e. B )
81 inelcm 
 |-  ( ( X e. A /\ X e. B ) -> ( A i^i B ) =/= (/) )
82 79 80 81 syl2anc 
 |-  ( ( ph /\ X e. A ) -> ( A i^i B ) =/= (/) )
83 82 neneqd 
 |-  ( ( ph /\ X e. A ) -> -. ( A i^i B ) = (/) )
84 78 83 pm2.65da 
 |-  ( ph -> -. X e. A )
85 84 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> -. X e. A )
86 77 85 eldifd 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> X e. ( h \ A ) )
87 simplr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> A C_ h )
88 9 1 2 73 74 75 86 87 plng3p 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> h = ( A E X ) )
89 72 88 sseqtrd 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> B C_ ( A E X ) )
90 8 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> Y e. B )
91 89 90 sseldd 
 |-  ( ( ( ( ph /\ h e. ran E ) /\ A C_ h ) /\ B C_ h ) -> Y e. ( A E X ) )
92 91 anasss 
 |-  ( ( ( ph /\ h e. ran E ) /\ ( A C_ h /\ B C_ h ) ) -> Y e. ( A E X ) )
93 34 simpld 
 |-  ( ph -> E. h e. ran E ( A C_ h /\ B C_ h ) )
94 92 93 r19.29a 
 |-  ( ph -> Y e. ( A E X ) )
95 28 84 eldifd 
 |-  ( ph -> X e. ( ( Base ` G ) \ A ) )
96 9 10 1 2 4 14 95 27 16 elplng 
 |-  ( ph -> ( Y e. ( A E X ) <-> ( Y e. A \/ Y ( ( hpG ` G ) ` A ) X \/ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) ) )
97 94 96 mpbid 
 |-  ( ph -> ( Y e. A \/ Y ( ( hpG ` G ) ` A ) X \/ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) )
98 97 adantr 
 |-  ( ( ph /\ Y =/= X ) -> ( Y e. A \/ Y ( ( hpG ` G ) ` A ) X \/ Y { <. a , b >. | ( ( a e. ( ( Base ` G ) \ A ) /\ b e. ( ( Base ` G ) \ A ) ) /\ E. s e. A s e. ( a ( Itv ` G ) b ) ) } X ) )
99 47 71 98 ecase13d 
 |-  ( ( ph /\ Y =/= X ) -> Y ( ( hpG ` G ) ` A ) X )
100 46 99 pm2.61dane 
 |-  ( ph -> Y ( ( hpG ` G ) ` A ) X )
101 9 10 1 4 14 16 27 28 100 hpgcom 
 |-  ( ph -> X ( ( hpG ` G ) ` A ) Y )