Metamath Proof Explorer

Theorem symquadprlng

Description: Symmetrical quadrilaterals are parallelograms. Theorem 12.18 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 )
symquadprlng.2 
|- ( ph -> ( X .- Y ) = ( Z .- W ) )
symquadprlng.3 
|- ( ph -> ( Y .- Z ) = ( W .- X ) )
symquadprlng.4 
|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
symquadprlng.5 
|- ( ph -> Y =/= W )
symquadprlng.6 
|- ( ph -> T e. ( X L Z ) )
symquadprlng.7 
|- ( ph -> T e. ( Y L W ) )
Assertion symquadprlng 
|- ( ph -> ( ( X L Y ) .|| ( Z L W ) /\ ( Y L Z ) .|| ( W L X ) ) )

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 symquadprlng.2 
 |-  ( ph -> ( X .- Y ) = ( Z .- W ) )
12 symquadprlng.3 
 |-  ( ph -> ( Y .- Z ) = ( W .- X ) )
13 symquadprlng.4 
 |-  ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
14 symquadprlng.5 
 |-  ( ph -> Y =/= W )
15 symquadprlng.6 
 |-  ( ph -> T e. ( X L Z ) )
16 symquadprlng.7 
 |-  ( ph -> T e. ( Y L W ) )
17 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
18 eqid 
 |-  ( midG ` G ) = ( midG ` G )
19 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
20 1 3 19 5 8 9 7 13 ncolrot2 
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
21 20 orsild 
 |-  ( ph -> -. Z e. ( X L Y ) )
22 9 21 eldifd 
 |-  ( ph -> Z e. ( P \ ( X L Y ) ) )
23 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
24 eqid 
 |-  ( ( pInvG ` G ) ` T ) = ( ( pInvG ` G ) ` T )
25 1 19 3 5 8 10 14 tgelrnln 
 |-  ( ph -> ( Y L W ) e. ran L )
26 1 3 19 5 25 16 tglnpt 
 |-  ( ph -> T e. P )
27 15 orcd 
 |-  ( ph -> ( T e. ( X L Z ) \/ X = Z ) )
28 16 orcd 
 |-  ( ph -> ( T e. ( Y L W ) \/ Y = W ) )
29 1 2 19 3 23 5 24 7 8 9 10 26 13 14 11 12 27 28 symquadlem 
 |-  ( ph -> X = ( ( ( pInvG ` G ) ` T ) ` Z ) )
30 1 3 19 5 8 9 7 13 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
31 1 2 19 5 30 9 7 23 26 ismidb 
 |-  ( ph -> ( X = ( ( ( pInvG ` G ) ` T ) ` Z ) <-> ( Z ( midG ` G ) X ) = T ) )
32 29 31 mpbid 
 |-  ( ph -> ( Z ( midG ` G ) X ) = T )
33 1 2 19 5 30 7 9 midcom 
 |-  ( ph -> ( X ( midG ` G ) Z ) = ( Z ( midG ` G ) X ) )
34 1 2 3 5 7 8 9 10 11 12 13 14 15 16 symquadprlnglem 
 |-  ( ph -> -. ( W e. ( Z L Y ) \/ Z = Y ) )
35 1 3 19 5 7 9 15 tglngne 
 |-  ( ph -> X =/= Z )
36 35 necomd 
 |-  ( ph -> Z =/= X )
37 1 2 19 5 7 8 9 10 11 tgcgrcomlr 
 |-  ( ph -> ( Y .- X ) = ( W .- Z ) )
38 37 eqcomd 
 |-  ( ph -> ( W .- Z ) = ( Y .- X ) )
39 1 2 19 5 8 9 10 7 12 tgcgrcomlr 
 |-  ( ph -> ( Z .- Y ) = ( X .- W ) )
40 1 3 19 5 8 10 26 28 colcom 
 |-  ( ph -> ( T e. ( W L Y ) \/ W = Y ) )
41 1 3 19 5 7 9 26 27 colcom 
 |-  ( ph -> ( T e. ( Z L X ) \/ Z = X ) )
42 1 2 19 3 23 5 24 10 9 8 7 26 34 36 38 39 40 41 symquadlem 
 |-  ( ph -> W = ( ( ( pInvG ` G ) ` T ) ` Y ) )
43 1 2 19 5 30 8 10 23 26 ismidb 
 |-  ( ph -> ( W = ( ( ( pInvG ` G ) ` T ) ` Y ) <-> ( Y ( midG ` G ) W ) = T ) )
44 42 43 mpbid 
 |-  ( ph -> ( Y ( midG ` G ) W ) = T )
45 32 33 44 3eqtr4d 
 |-  ( ph -> ( X ( midG ` G ) Z ) = ( Y ( midG ` G ) W ) )
46 1 19 3 5 7 8 9 13 ncolne1 
 |-  ( ph -> X =/= Y )
47 1 3 17 4 18 5 6 7 8 22 10 45 46 prlngmid2 
 |-  ( ph -> ( X L Y ) .|| ( Z L W ) )
48 34 orsild 
 |-  ( ph -> -. W e. ( Z L Y ) )
49 34 orsird 
 |-  ( ph -> -. Z = Y )
50 49 neqned 
 |-  ( ph -> Z =/= Y )
51 1 19 3 5 9 8 50 tglinecom 
 |-  ( ph -> ( Z L Y ) = ( Y L Z ) )
52 48 51 neleqtrd 
 |-  ( ph -> -. W e. ( Y L Z ) )
53 10 52 eldifd 
 |-  ( ph -> W e. ( P \ ( Y L Z ) ) )
54 44 32 eqtr4d 
 |-  ( ph -> ( Y ( midG ` G ) W ) = ( Z ( midG ` G ) X ) )
55 50 necomd 
 |-  ( ph -> Y =/= Z )
56 1 3 17 4 18 5 6 8 9 53 7 54 55 prlngmid2 
 |-  ( ph -> ( Y L Z ) .|| ( W L X ) )
57 47 56 jca 
 |-  ( ph -> ( ( X L Y ) .|| ( Z L W ) /\ ( Y L Z ) .|| ( W L X ) ) )