Metamath Proof Explorer

Theorem symquadprlnglem

Description: Lemma for symquadprlnglem . (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses symquadprlnglem.p 
|- P = ( Base ` G )
symquadprlnglem.d 
|- .- = ( dist ` G )
symquadprlnglem.l 
|- L = ( LineG ` G )
symquadprlnglem.g 
|- ( ph -> G e. TarskiG )
symquadprlnglem.x 
|- ( ph -> X e. P )
symquadprlnglem.y 
|- ( ph -> Y e. P )
symquadprlnglem.z 
|- ( ph -> Z e. P )
symquadprlnglem.w 
|- ( ph -> W e. P )
symquadprlnglem.1 
|- ( ph -> ( X .- Y ) = ( Z .- W ) )
symquadprlnglem.2 
|- ( ph -> ( Y .- Z ) = ( W .- X ) )
symquadprlnglem.3 
|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
symquadprlnglem.4 
|- ( ph -> Y =/= W )
symquadprlnglem.5 
|- ( ph -> T e. ( X L Z ) )
symquadprlnglem.6 
|- ( ph -> T e. ( Y L W ) )
Assertion symquadprlnglem 
|- ( ph -> -. ( W e. ( Z L Y ) \/ Z = Y ) )

Proof

Step Hyp Ref Expression
1 symquadprlnglem.p 
 |-  P = ( Base ` G )
2 symquadprlnglem.d 
 |-  .- = ( dist ` G )
3 symquadprlnglem.l 
 |-  L = ( LineG ` G )
4 symquadprlnglem.g 
 |-  ( ph -> G e. TarskiG )
5 symquadprlnglem.x 
 |-  ( ph -> X e. P )
6 symquadprlnglem.y 
 |-  ( ph -> Y e. P )
7 symquadprlnglem.z 
 |-  ( ph -> Z e. P )
8 symquadprlnglem.w 
 |-  ( ph -> W e. P )
9 symquadprlnglem.1 
 |-  ( ph -> ( X .- Y ) = ( Z .- W ) )
10 symquadprlnglem.2 
 |-  ( ph -> ( Y .- Z ) = ( W .- X ) )
11 symquadprlnglem.3 
 |-  ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
12 symquadprlnglem.4 
 |-  ( ph -> Y =/= W )
13 symquadprlnglem.5 
 |-  ( ph -> T e. ( X L Z ) )
14 symquadprlnglem.6 
 |-  ( ph -> T e. ( Y L W ) )
15 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
16 1 3 15 4 5 7 13 tglngne 
 |-  ( ph -> X =/= Z )
17 16 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> X =/= Z )
18 4 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> G e. TarskiG )
19 1 15 3 4 6 8 12 tgelrnln 
 |-  ( ph -> ( Y L W ) e. ran L )
20 1 3 15 4 19 14 tglnpt 
 |-  ( ph -> T e. P )
21 20 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> T e. P )
22 7 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> Z e. P )
23 5 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> X e. P )
24 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
25 eqid 
 |-  ( ( pInvG ` G ) ` T ) = ( ( pInvG ` G ) ` T )
26 13 orcd 
 |-  ( ph -> ( T e. ( X L Z ) \/ X = Z ) )
27 14 orcd 
 |-  ( ph -> ( T e. ( Y L W ) \/ Y = W ) )
28 1 2 15 3 24 4 25 5 6 7 8 20 11 12 9 10 26 27 symquadlem 
 |-  ( ph -> X = ( ( ( pInvG ` G ) ` T ) ` Z ) )
29 28 oveq2d 
 |-  ( ph -> ( T .- X ) = ( T .- ( ( ( pInvG ` G ) ` T ) ` Z ) ) )
30 1 2 15 3 24 4 20 25 7 mircgr 
 |-  ( ph -> ( T .- ( ( ( pInvG ` G ) ` T ) ` Z ) ) = ( T .- Z ) )
31 29 30 eqtr2d 
 |-  ( ph -> ( T .- Z ) = ( T .- X ) )
32 31 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> ( T .- Z ) = ( T .- X ) )
33 simpr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> T = Z )
34 1 2 15 18 21 22 21 23 32 33 tgcgreq 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> T = X )
35 34 33 eqtr3d 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> X = Z )
36 nne 
 |-  ( -. X =/= Z <-> X = Z )
37 35 36 sylibr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T = Z ) -> -. X =/= Z )
38 17 37 pm2.65da 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> -. T = Z )
39 38 neqned 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> T =/= Z )
40 4 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> G e. TarskiG )
41 7 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> Z e. P )
42 5 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> X e. P )
43 6 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> Y e. P )
44 20 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> T e. P )
45 4 adantr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> G e. TarskiG )
46 7 adantr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> Z e. P )
47 6 adantr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> Y e. P )
48 20 adantr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> T e. P )
49 8 adantr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> W e. P )
50 1 15 3 4 6 8 12 tglinecom 
 |-  ( ph -> ( Y L W ) = ( W L Y ) )
51 14 50 eleqtrd 
 |-  ( ph -> T e. ( W L Y ) )
52 51 adantr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> T e. ( W L Y ) )
53 simpr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> ( W e. ( Z L Y ) \/ Z = Y ) )
54 1 3 15 45 46 47 49 53 colcom 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> ( W e. ( Y L Z ) \/ Y = Z ) )
55 1 15 3 45 48 49 47 46 52 54 coltr 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> ( T e. ( Y L Z ) \/ Y = Z ) )
56 1 3 15 45 47 46 48 55 colcom 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> ( T e. ( Z L Y ) \/ Z = Y ) )
57 1 3 15 45 46 47 48 56 colrot2 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> ( Y e. ( T L Z ) \/ T = Z ) )
58 57 adantr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> ( Y e. ( T L Z ) \/ T = Z ) )
59 simpr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> T =/= Z )
60 59 neneqd 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> -. T = Z )
61 58 60 olcnd 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> Y e. ( T L Z ) )
62 1 3 15 4 5 7 20 26 colcom 
 |-  ( ph -> ( T e. ( Z L X ) \/ Z = X ) )
63 62 ad2antrr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> ( T e. ( Z L X ) \/ Z = X ) )
64 1 15 3 40 43 44 41 42 61 63 coltr 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> ( Y e. ( Z L X ) \/ Z = X ) )
65 1 3 15 40 41 42 43 64 colrot2 
 |-  ( ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) /\ T =/= Z ) -> ( X e. ( Y L Z ) \/ Y = Z ) )
66 39 65 mpdan 
 |-  ( ( ph /\ ( W e. ( Z L Y ) \/ Z = Y ) ) -> ( X e. ( Y L Z ) \/ Y = Z ) )
67 11 66 mtand 
 |-  ( ph -> -. ( W e. ( Z L Y ) \/ Z = Y ) )