Metamath Proof Explorer

Theorem prlngeq

Description: Playfair's axiom, written as an equality: if two different lines are parallel to a given line at a given point, they are equal. (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses prlngeq.p 
|- P = ( Base ` G )
prlngeq.r 
|- .|| = ( parlnG ` G )
prlngeq.g 
|- ( ph -> G e. TarskiG )
prlngeq.1 
|- ( ph -> G e. TarskiGE )
prlngeq.b 
|- ( ph -> A .|| B )
prlngeq.c 
|- ( ph -> A .|| C )
prlngeq.2 
|- ( ph -> X e. B )
prlngeq.3 
|- ( ph -> X e. C )
Assertion prlngeq 
|- ( ph -> B = C )

Proof

Step Hyp Ref Expression
1 prlngeq.p 
 |-  P = ( Base ` G )
2 prlngeq.r 
 |-  .|| = ( parlnG ` G )
3 prlngeq.g 
 |-  ( ph -> G e. TarskiG )
4 prlngeq.1 
 |-  ( ph -> G e. TarskiGE )
5 prlngeq.b 
 |-  ( ph -> A .|| B )
6 prlngeq.c 
 |-  ( ph -> A .|| C )
7 prlngeq.2 
 |-  ( ph -> X e. B )
8 prlngeq.3 
 |-  ( ph -> X e. C )
9 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
10 9 2 3 5 prlngrcl1 
 |-  ( ph -> A e. ran ( LineG ` G ) )
11 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
12 9 2 3 5 prlngrcl2 
 |-  ( ph -> B e. ran ( LineG ` G ) )
13 1 9 11 3 12 7 tglnpt 
 |-  ( ph -> X e. P )
14 1 9 2 3 10 13 4 prlngmo2 
 |-  ( ph -> E* b e. ran ( LineG ` G ) ( A .|| b /\ X e. b ) )
15 5 7 jca 
 |-  ( ph -> ( A .|| B /\ X e. B ) )
16 9 2 3 6 prlngrcl2 
 |-  ( ph -> C e. ran ( LineG ` G ) )
17 6 8 jca 
 |-  ( ph -> ( A .|| C /\ X e. C ) )
18 breq2 
 |-  ( b = B -> ( A .|| b <-> A .|| B ) )
19 eleq2 
 |-  ( b = B -> ( X e. b <-> X e. B ) )
20 18 19 anbi12d 
 |-  ( b = B -> ( ( A .|| b /\ X e. b ) <-> ( A .|| B /\ X e. B ) ) )
21 breq2 
 |-  ( b = C -> ( A .|| b <-> A .|| C ) )
22 eleq2 
 |-  ( b = C -> ( X e. b <-> X e. C ) )
23 21 22 anbi12d 
 |-  ( b = C -> ( ( A .|| b /\ X e. b ) <-> ( A .|| C /\ X e. C ) ) )
24 20 23 rmoi 
 |-  ( ( E* b e. ran ( LineG ` G ) ( A .|| b /\ X e. b ) /\ ( B e. ran ( LineG ` G ) /\ ( A .|| B /\ X e. B ) ) /\ ( C e. ran ( LineG ` G ) /\ ( A .|| C /\ X e. C ) ) ) -> B = C )
25 14 12 15 16 17 24 syl122anc 
 |-  ( ph -> B = C )