Metamath Proof Explorer

Theorem prlngsymquadopp

Description: In parallelograms, opposing vertices are on opposite sides of the diagonal. Second part of Theorem 12.19 of Schwabhauser p. 126. (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 ) )
prlngsymquadopp.o 
|- O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) }
prlngsymquadopp.i 
|- I = ( Itv ` G )
Assertion prlngsymquadopp 
|- ( ph -> W O Y )

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 prlngsymquadopp.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) }
15 prlngsymquadopp.i 
 |-  I = ( Itv ` G )
16 1 3 15 5 8 9 7 11 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
17 1 2 15 5 16 7 9 midcl 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. P )
18 1 15 3 5 7 8 9 11 ncolne2 
 |-  ( ph -> X =/= Z )
19 1 2 15 5 16 7 9 midbtwn 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. ( X I Z ) )
20 1 15 3 5 7 9 17 18 19 btwnlng1 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. ( X L Z ) )
21 1 3 15 5 8 9 7 11 ncolcom 
 |-  ( ph -> -. ( X e. ( Z L Y ) \/ Z = Y ) )
22 1 3 15 5 9 8 7 21 ncolrot2 
 |-  ( ph -> -. ( Y e. ( X L Z ) \/ X = Z ) )
23 22 orsild 
 |-  ( ph -> -. Y e. ( X L Z ) )
24 1 15 3 5 8 7 9 22 ncolne2 
 |-  ( ph -> Y =/= Z )
25 1 15 3 5 8 9 24 tglinerflx1 
 |-  ( ph -> Y e. ( Y L Z ) )
26 25 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Y e. ( Y L Z ) )
27 5 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> G e. TarskiG )
28 6 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> G e. TarskiGE )
29 13 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( Y L Z ) .|| ( W L X ) )
30 7 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> X e. P )
31 10 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> W e. P )
32 3 4 5 13 prlngrcl2 
 |-  ( ph -> ( W L X ) e. ran L )
33 1 15 3 5 10 7 32 tglnne 
 |-  ( ph -> W =/= X )
34 33 necomd 
 |-  ( ph -> X =/= W )
35 34 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> X =/= W )
36 9 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Z e. P )
37 18 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> X =/= Z )
38 37 necomd 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Z =/= X )
39 simpr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> W e. ( X L Z ) )
40 1 15 3 27 30 36 37 tglinecom 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( X L Z ) = ( Z L X ) )
41 39 40 eleqtrd 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> W e. ( Z L X ) )
42 1 15 3 27 30 31 36 35 41 38 lnrot1 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Z e. ( X L W ) )
43 1 15 3 27 30 31 35 36 38 42 tglineelsb2 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( X L W ) = ( X L Z ) )
44 1 15 3 5 7 10 34 tglinecom 
 |-  ( ph -> ( X L W ) = ( W L X ) )
45 44 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( X L W ) = ( W L X ) )
46 43 45 eqtr3d 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( X L Z ) = ( W L X ) )
47 29 46 breqtrrd 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( Y L Z ) .|| ( X L Z ) )
48 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
49 3 4 5 13 prlngrcl1 
 |-  ( ph -> ( Y L Z ) e. ran L )
50 3 48 4 5 49 prlngref 
 |-  ( ph -> ( Y L Z ) .|| ( Y L Z ) )
51 50 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( Y L Z ) .|| ( Y L Z ) )
52 42 43 eleqtrd 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Z e. ( X L Z ) )
53 1 15 3 5 8 9 24 tglinerflx2 
 |-  ( ph -> Z e. ( Y L Z ) )
54 53 adantr 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Z e. ( Y L Z ) )
55 1 4 27 28 47 51 52 54 prlngeq 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> ( X L Z ) = ( Y L Z ) )
56 26 55 eleqtrrd 
 |-  ( ( ph /\ W e. ( X L Z ) ) -> Y e. ( X L Z ) )
57 23 56 mtand 
 |-  ( ph -> -. W e. ( X L Z ) )
58 eqid 
 |-  ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 58 prlngsymquadlem 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) = W )
60 59 eqcomd 
 |-  ( ph -> W = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) )
61 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
62 1 2 15 5 16 8 10 61 17 ismidb 
 |-  ( ph -> ( W = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) <-> ( Y ( midG ` G ) W ) = ( X ( midG ` G ) Z ) ) )
63 60 62 mpbid 
 |-  ( ph -> ( Y ( midG ` G ) W ) = ( X ( midG ` G ) Z ) )
64 1 2 15 5 16 8 10 midcl 
 |-  ( ph -> ( Y ( midG ` G ) W ) e. P )
65 1 2 15 5 16 8 10 midbtwn 
 |-  ( ph -> ( Y ( midG ` G ) W ) e. ( Y I W ) )
66 1 2 15 5 8 64 10 65 tgbtwncom 
 |-  ( ph -> ( Y ( midG ` G ) W ) e. ( W I Y ) )
67 63 66 eqeltrrd 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. ( W I Y ) )
68 1 2 15 14 10 8 20 57 23 67 islnoppd 
 |-  ( ph -> W O Y )