Metamath Proof Explorer

Theorem prlngsymquadlem

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

Ref Expression
Hypotheses symquadprlng.p 
|- P = ( Base ` G )
symquadprlng.d 
|- .- = ( dist ` G )
symquadprlng.l 
|- L = ( LineG ` G )
symquadprlng.r 
|- .|| = ( parlnG ` G )
symquadprlng.g 
|- ( ph -> G e. TarskiG )
symquadprlng.1 
|- ( ph -> G e. TarskiGE )
symquadprlng.x 
|- ( ph -> X e. P )
symquadprlng.y 
|- ( ph -> Y e. P )
symquadprlng.z 
|- ( ph -> Z e. P )
symquadprlng.w 
|- ( ph -> W e. P )
prlngsymquad.2 
|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
prlngsymquad.3 
|- ( ph -> ( X L Y ) .|| ( Z L W ) )
prlngsymquad.4 
|- ( ph -> ( Y L Z ) .|| ( W L X ) )
prlngsymquadlem.t 
|- T = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y )
Assertion prlngsymquadlem 
|- ( ph -> T = W )

Proof

Step Hyp Ref Expression
1 symquadprlng.p 
 |-  P = ( Base ` G )
2 symquadprlng.d 
 |-  .- = ( dist ` G )
3 symquadprlng.l 
 |-  L = ( LineG ` G )
4 symquadprlng.r 
 |-  .|| = ( parlnG ` G )
5 symquadprlng.g 
 |-  ( ph -> G e. TarskiG )
6 symquadprlng.1 
 |-  ( ph -> G e. TarskiGE )
7 symquadprlng.x 
 |-  ( ph -> X e. P )
8 symquadprlng.y 
 |-  ( ph -> Y e. P )
9 symquadprlng.z 
 |-  ( ph -> Z e. P )
10 symquadprlng.w 
 |-  ( ph -> W e. P )
11 prlngsymquad.2 
 |-  ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
12 prlngsymquad.3 
 |-  ( ph -> ( X L Y ) .|| ( Z L W ) )
13 prlngsymquad.4 
 |-  ( ph -> ( Y L Z ) .|| ( W L X ) )
14 prlngsymquadlem.t 
 |-  T = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y )
15 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
16 3 4 5 13 prlngrcl2 
 |-  ( ph -> ( W L X ) e. ran L )
17 1 15 3 5 10 7 16 tglnne 
 |-  ( ph -> W =/= X )
18 1 15 3 5 10 7 17 tglinecom 
 |-  ( ph -> ( W L X ) = ( X L W ) )
19 18 16 eqeltrrd 
 |-  ( ph -> ( X L W ) e. ran L )
20 3 4 5 12 prlngrcl2 
 |-  ( ph -> ( Z L W ) e. ran L )
21 1 15 3 5 7 8 9 10 11 tglineneq 
 |-  ( ph -> ( X L Y ) =/= ( Z L W ) )
22 5 ad2antrr 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> G e. TarskiG )
23 12 ad2antrr 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> ( X L Y ) .|| ( Z L W ) )
24 simpr 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> ( X L Y ) =/= ( Z L W ) )
25 3 4 22 23 24 prlngin0 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> ( ( X L Y ) i^i ( Z L W ) ) = (/) )
26 1 15 3 5 7 8 9 11 ncolne1 
 |-  ( ph -> X =/= Y )
27 1 15 3 5 7 8 26 tglinerflx1 
 |-  ( ph -> X e. ( X L Y ) )
28 27 ad2antrr 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> X e. ( X L Y ) )
29 17 necomd 
 |-  ( ph -> X =/= W )
30 1 15 3 5 7 10 29 tglinerflx1 
 |-  ( ph -> X e. ( X L W ) )
31 30 ad2antrr 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> X e. ( X L W ) )
32 simplr 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> ( X L W ) = ( Z L W ) )
33 31 32 eleqtrd 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> X e. ( Z L W ) )
34 28 33 elind 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> X e. ( ( X L Y ) i^i ( Z L W ) ) )
35 34 ne0d 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> ( ( X L Y ) i^i ( Z L W ) ) =/= (/) )
36 35 neneqd 
 |-  ( ( ( ph /\ ( X L W ) = ( Z L W ) ) /\ ( X L Y ) =/= ( Z L W ) ) -> -. ( ( X L Y ) i^i ( Z L W ) ) = (/) )
37 25 36 pm2.65da 
 |-  ( ( ph /\ ( X L W ) = ( Z L W ) ) -> -. ( X L Y ) =/= ( Z L W ) )
38 nne 
 |-  ( -. ( X L Y ) =/= ( Z L W ) <-> ( X L Y ) = ( Z L W ) )
39 37 38 sylib 
 |-  ( ( ph /\ ( X L W ) = ( Z L W ) ) -> ( X L Y ) = ( Z L W ) )
40 21 39 mteqand 
 |-  ( ph -> ( X L W ) =/= ( Z L W ) )
41 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
42 1 3 15 5 8 9 7 11 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
43 1 2 15 5 42 7 9 midcl 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. P )
44 eqid 
 |-  ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) = ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) )
45 1 2 15 3 41 5 43 44 8 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) e. P )
46 14 45 eqeltrid 
 |-  ( ph -> T e. P )
47 3 4 5 13 prlngrcl1 
 |-  ( ph -> ( Y L Z ) e. ran L )
48 1 15 3 5 8 9 47 tglnne 
 |-  ( ph -> Y =/= Z )
49 48 necomd 
 |-  ( ph -> Z =/= Y )
50 1 41 44 5 43 9 8 mirleqb 
 |-  ( ph -> ( Z = Y <-> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) )
51 50 necon3bid 
 |-  ( ph -> ( Z =/= Y <-> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) =/= ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) )
52 49 51 mpbid 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) =/= ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) )
53 eqidd 
 |-  ( ph -> ( X ( midG ` G ) Z ) = ( X ( midG ` G ) Z ) )
54 1 2 15 5 42 7 9 41 43 ismidb 
 |-  ( ph -> ( Z = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) <-> ( X ( midG ` G ) Z ) = ( X ( midG ` G ) Z ) ) )
55 53 54 mpbird 
 |-  ( ph -> Z = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) )
56 55 eqcomd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) = Z )
57 1 2 15 3 41 5 43 44 7 56 mircom 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) = X )
58 14 eqcomi 
 |-  ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) = T
59 58 a1i 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) = T )
60 52 57 59 3netr3d 
 |-  ( ph -> X =/= T )
61 1 15 3 5 7 46 60 tglinerflx2 
 |-  ( ph -> T e. ( X L T ) )
62 1 41 44 5 43 7 8 mirleqb 
 |-  ( ph -> ( X = Y <-> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) )
63 62 necon3bid 
 |-  ( ph -> ( X =/= Y <-> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) =/= ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) )
64 26 63 mpbid 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) =/= ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) )
65 64 56 59 3netr3d 
 |-  ( ph -> Z =/= T )
66 1 15 3 5 9 46 65 tglinerflx2 
 |-  ( ph -> T e. ( Z L T ) )
67 61 66 elind 
 |-  ( ph -> T e. ( ( X L T ) i^i ( Z L T ) ) )
68 1 15 3 5 8 9 48 tglinecom 
 |-  ( ph -> ( Y L Z ) = ( Z L Y ) )
69 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
70 eqid 
 |-  ( midG ` G ) = ( midG ` G )
71 1 3 15 5 8 9 7 11 ncolcom 
 |-  ( ph -> -. ( X e. ( Z L Y ) \/ Z = Y ) )
72 71 orsild 
 |-  ( ph -> -. X e. ( Z L Y ) )
73 7 72 eldifd 
 |-  ( ph -> X e. ( P \ ( Z L Y ) ) )
74 1 2 15 5 42 9 7 midcom 
 |-  ( ph -> ( Z ( midG ` G ) X ) = ( X ( midG ` G ) Z ) )
75 1 2 15 5 42 8 46 41 43 ismidb 
 |-  ( ph -> ( T = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) <-> ( Y ( midG ` G ) T ) = ( X ( midG ` G ) Z ) ) )
76 14 75 mpbii 
 |-  ( ph -> ( Y ( midG ` G ) T ) = ( X ( midG ` G ) Z ) )
77 76 eqcomd 
 |-  ( ph -> ( X ( midG ` G ) Z ) = ( Y ( midG ` G ) T ) )
78 74 77 eqtrd 
 |-  ( ph -> ( Z ( midG ` G ) X ) = ( Y ( midG ` G ) T ) )
79 1 3 69 4 70 5 6 9 8 73 46 78 49 prlngmid2 
 |-  ( ph -> ( Z L Y ) .|| ( X L T ) )
80 68 79 eqbrtrd 
 |-  ( ph -> ( Y L Z ) .|| ( X L T ) )
81 13 18 breqtrd 
 |-  ( ph -> ( Y L Z ) .|| ( X L W ) )
82 1 15 3 5 7 46 60 tglinerflx1 
 |-  ( ph -> X e. ( X L T ) )
83 1 4 5 6 80 81 82 30 prlngeq 
 |-  ( ph -> ( X L T ) = ( X L W ) )
84 1 3 15 5 8 9 7 11 ncolrot2 
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
85 84 orsild 
 |-  ( ph -> -. Z e. ( X L Y ) )
86 9 85 eldifd 
 |-  ( ph -> Z e. ( P \ ( X L Y ) ) )
87 1 3 69 4 70 5 6 7 8 86 46 77 26 prlngmid2 
 |-  ( ph -> ( X L Y ) .|| ( Z L T ) )
88 1 15 3 5 9 46 65 tglinerflx1 
 |-  ( ph -> Z e. ( Z L T ) )
89 1 15 3 5 9 10 20 tglnne 
 |-  ( ph -> Z =/= W )
90 1 15 3 5 9 10 89 tglinerflx1 
 |-  ( ph -> Z e. ( Z L W ) )
91 1 4 5 6 87 12 88 90 prlngeq 
 |-  ( ph -> ( Z L T ) = ( Z L W ) )
92 83 91 ineq12d 
 |-  ( ph -> ( ( X L T ) i^i ( Z L T ) ) = ( ( X L W ) i^i ( Z L W ) ) )
93 67 92 eleqtrd 
 |-  ( ph -> T e. ( ( X L W ) i^i ( Z L W ) ) )
94 1 15 3 5 7 10 29 tglinerflx2 
 |-  ( ph -> W e. ( X L W ) )
95 1 15 3 5 9 10 89 tglinerflx2 
 |-  ( ph -> W e. ( Z L W ) )
96 94 95 elind 
 |-  ( ph -> W e. ( ( X L W ) i^i ( Z L W ) ) )
97 1 15 3 5 19 20 40 93 96 tglineineq 
 |-  ( ph -> T = W )