Metamath Proof Explorer

Theorem prlngmo2

Description: Playfair's axiom, without the restriction that the point X is outside of the line A . Theorem 12.11 of Schwabhauser p. 123. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses prlngmo2.p 
|- P = ( Base ` G )
prlngmo2.l 
|- L = ( LineG ` G )
prlngmo2.r 
|- .|| = ( parlnG ` G )
prlngmo2.g 
|- ( ph -> G e. TarskiG )
prlngmo2.a 
|- ( ph -> A e. ran L )
prlngmo2.x 
|- ( ph -> X e. P )
prlngmo2.1 
|- ( ph -> G e. TarskiGE )
Assertion prlngmo2 
|- ( ph -> E* b e. ran L ( A .|| b /\ X e. b ) )

Proof

Step Hyp Ref Expression
1 prlngmo2.p 
 |-  P = ( Base ` G )
2 prlngmo2.l 
 |-  L = ( LineG ` G )
3 prlngmo2.r 
 |-  .|| = ( parlnG ` G )
4 prlngmo2.g 
 |-  ( ph -> G e. TarskiG )
5 prlngmo2.a 
 |-  ( ph -> A e. ran L )
6 prlngmo2.x 
 |-  ( ph -> X e. P )
7 prlngmo2.1 
 |-  ( ph -> G e. TarskiGE )
8 eqeq2 
 |-  ( a = A -> ( b = a <-> b = A ) )
9 8 imbi2d 
 |-  ( a = A -> ( ( ( A .|| b /\ X e. b ) -> b = a ) <-> ( ( A .|| b /\ X e. b ) -> b = A ) ) )
10 9 ralbidv 
 |-  ( a = A -> ( A. b e. ran L ( ( A .|| b /\ X e. b ) -> b = a ) <-> A. b e. ran L ( ( A .|| b /\ X e. b ) -> b = A ) ) )
11 5 adantr 
 |-  ( ( ph /\ X e. A ) -> A e. ran L )
12 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> G e. TarskiG )
13 simpllr 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> A .|| b )
14 simpr 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> -. b = A )
15 14 neqned 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> b =/= A )
16 15 necomd 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> A =/= b )
17 2 3 12 13 16 prlngin0 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> ( A i^i b ) = (/) )
18 simp-5r 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> X e. A )
19 simplr 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> X e. b )
20 18 19 elind 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> X e. ( A i^i b ) )
21 20 ne0d 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> ( A i^i b ) =/= (/) )
22 21 neneqd 
 |-  ( ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) /\ -. b = A ) -> -. ( A i^i b ) = (/) )
23 17 22 condan 
 |-  ( ( ( ( ( ph /\ X e. A ) /\ b e. ran L ) /\ A .|| b ) /\ X e. b ) -> b = A )
24 23 expl 
 |-  ( ( ( ph /\ X e. A ) /\ b e. ran L ) -> ( ( A .|| b /\ X e. b ) -> b = A ) )
25 24 ralrimiva 
 |-  ( ( ph /\ X e. A ) -> A. b e. ran L ( ( A .|| b /\ X e. b ) -> b = A ) )
26 10 11 25 rspcedvdw 
 |-  ( ( ph /\ X e. A ) -> E. a e. ran L A. b e. ran L ( ( A .|| b /\ X e. b ) -> b = a ) )
27 nfv 
 |-  F/ a ( A .|| b /\ X e. b )
28 27 rmo2i 
 |-  ( E. a e. ran L A. b e. ran L ( ( A .|| b /\ X e. b ) -> b = a ) -> E* b e. ran L ( A .|| b /\ X e. b ) )
29 26 28 syl 
 |-  ( ( ph /\ X e. A ) -> E* b e. ran L ( A .|| b /\ X e. b ) )
30 4 adantr 
 |-  ( ( ph /\ -. X e. A ) -> G e. TarskiG )
31 5 adantr 
 |-  ( ( ph /\ -. X e. A ) -> A e. ran L )
32 6 adantr 
 |-  ( ( ph /\ -. X e. A ) -> X e. P )
33 simpr 
 |-  ( ( ph /\ -. X e. A ) -> -. X e. A )
34 32 33 eldifd 
 |-  ( ( ph /\ -. X e. A ) -> X e. ( P \ A ) )
35 7 adantr 
 |-  ( ( ph /\ -. X e. A ) -> G e. TarskiGE )
36 1 2 3 30 31 34 35 prlngmo 
 |-  ( ( ph /\ -. X e. A ) -> E* b e. ran L ( A .|| b /\ X e. b ) )
37 29 36 pm2.61dan 
 |-  ( ph -> E* b e. ran L ( A .|| b /\ X e. b ) )