Metamath Proof Explorer

Theorem prlngsymquad

Description: All parallelograms are symmetric quadrilaterals. First 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 ) )
Assertion prlngsymquad 
|- ( ph -> ( ( X .- Y ) = ( Z .- W ) /\ ( Y .- Z ) = ( W .- 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 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 eqidd 
 |-  ( ph -> ( X ( midG ` G ) Z ) = ( X ( midG ` G ) Z ) )
15 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
16 1 3 15 5 8 9 7 11 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
17 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
18 1 2 15 5 16 7 9 midcl 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. P )
19 1 2 15 5 16 7 9 17 18 ismidb 
 |-  ( ph -> ( Z = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) <-> ( X ( midG ` G ) Z ) = ( X ( midG ` G ) Z ) ) )
20 14 19 mpbird 
 |-  ( ph -> Z = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) )
21 20 eqcomd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) = Z )
22 21 oveq1d 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) .- ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) = ( Z .- ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) )
23 eqid 
 |-  ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) = ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) )
24 1 2 15 3 17 5 18 23 7 8 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` X ) .- ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) = ( X .- Y ) )
25 eqid 
 |-  ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) = ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 25 prlngsymquadlem 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) = W )
27 26 oveq2d 
 |-  ( ph -> ( Z .- ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) ) = ( Z .- W ) )
28 22 24 27 3eqtr3d 
 |-  ( ph -> ( X .- Y ) = ( Z .- W ) )
29 1 2 15 3 17 5 18 23 7 21 mircom 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) = X )
30 29 oveq2d 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) .- ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) ) = ( ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) .- X ) )
31 1 2 15 3 17 5 18 23 8 9 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) .- ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Z ) ) = ( Y .- Z ) )
32 26 oveq1d 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( X ( midG ` G ) Z ) ) ` Y ) .- X ) = ( W .- X ) )
33 30 31 32 3eqtr3d 
 |-  ( ph -> ( Y .- Z ) = ( W .- X ) )
34 28 33 jca 
 |-  ( ph -> ( ( X .- Y ) = ( Z .- W ) /\ ( Y .- Z ) = ( W .- X ) ) )