Metamath Proof Explorer

Theorem prlngsym

Description: Parallelism is symmetric. Theorem 12.5 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 18-Jun-2026)

Ref Expression
Hypotheses brprlng.l 
|- L = ( LineG ` G )
brprlng.e 
|- E = ( PlnG ` G )
brprlng.p 
|- .|| = ( parlnG ` G )
brprlng.g 
|- ( ph -> G e. V )
prlngsym.1 
|- ( ph -> A .|| B )
Assertion prlngsym 
|- ( ph -> B .|| A )

Proof

Step Hyp Ref Expression
1 brprlng.l 
 |-  L = ( LineG ` G )
2 brprlng.e 
 |-  E = ( PlnG ` G )
3 brprlng.p 
 |-  .|| = ( parlnG ` G )
4 brprlng.g 
 |-  ( ph -> G e. V )
5 prlngsym.1 
 |-  ( ph -> A .|| B )
6 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 ) = (/) ) ) ) ) )
7 5 6 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 ) = (/) ) ) ) )
8 7 simpld 
 |-  ( ph -> ( A e. ran L /\ B e. ran L ) )
9 8 simprd 
 |-  ( ph -> B e. ran L )
10 8 simpld 
 |-  ( ph -> A e. ran L )
11 eqcom 
 |-  ( A = B <-> B = A )
12 11 bilani 
 |-  ( ( ph /\ A = B ) -> B = A )
13 ancom 
 |-  ( ( A C_ h /\ B C_ h ) <-> ( B C_ h /\ A C_ h ) )
14 13 a1i 
 |-  ( ph -> ( ( A C_ h /\ B C_ h ) <-> ( B C_ h /\ A C_ h ) ) )
15 14 rexbidv 
 |-  ( ph -> ( E. h e. ran E ( A C_ h /\ B C_ h ) <-> E. h e. ran E ( B C_ h /\ A C_ h ) ) )
16 incom 
 |-  ( A i^i B ) = ( B i^i A )
17 16 a1i 
 |-  ( ph -> ( A i^i B ) = ( B i^i A ) )
18 17 eqeq1d 
 |-  ( ph -> ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) ) )
19 15 18 anbi12d 
 |-  ( ph -> ( ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) <-> ( E. h e. ran E ( B C_ h /\ A C_ h ) /\ ( B i^i A ) = (/) ) ) )
20 19 biimpa 
 |-  ( ( ph /\ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) -> ( E. h e. ran E ( B C_ h /\ A C_ h ) /\ ( B i^i A ) = (/) ) )
21 7 simprd 
 |-  ( ph -> ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) )
22 12 20 21 orim12da 
 |-  ( ph -> ( B = A \/ ( E. h e. ran E ( B C_ h /\ A C_ h ) /\ ( B i^i A ) = (/) ) ) )
23 9 10 22 jca31 
 |-  ( ph -> ( ( B e. ran L /\ A e. ran L ) /\ ( B = A \/ ( E. h e. ran E ( B C_ h /\ A C_ h ) /\ ( B i^i A ) = (/) ) ) ) )
24 1 2 3 4 brprlng 
 |-  ( ph -> ( B .|| A <-> ( ( B e. ran L /\ A e. ran L ) /\ ( B = A \/ ( E. h e. ran E ( B C_ h /\ A C_ h ) /\ ( B i^i A ) = (/) ) ) ) ) )
25 23 24 mpbird 
 |-  ( ph -> B .|| A )