Metamath Proof Explorer

Theorem symquadmid

Description: In a symmetrical quadrilateral, the midpoints of the diagonals coincide. Corollary of Lemma 7.21 of Schwabhauser p. 52. (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses symquadmid.p 
|- P = ( Base ` G )
symquadmid.d 
|- .- = ( dist ` G )
symquadmid.i 
|- I = ( Itv ` G )
symquadmid.l 
|- L = ( LineG ` G )
symquadmid.m 
|- M = ( midG ` G )
symquadmid.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 ) ) }
symquadmid.g 
|- ( ph -> G e. TarskiG )
symquadmid.x 
|- ( ph -> X e. P )
symquadmid.y 
|- ( ph -> Y e. P )
symquadmid.z 
|- ( ph -> Z e. P )
symquadmid.w 
|- ( ph -> W e. P )
symquadmid.2 
|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
symquadmid.3 
|- ( ph -> Y =/= W )
symquadmid.4 
|- ( ph -> ( X .- Y ) = ( Z .- W ) )
symquadmid.5 
|- ( ph -> ( Y .- Z ) = ( W .- X ) )
symquadmid.6 
|- ( ph -> Y O W )
Assertion symquadmid 
|- ( ph -> ( X M Z ) = ( Y M W ) )

Proof

Step Hyp Ref Expression
1 symquadmid.p 
 |-  P = ( Base ` G )
2 symquadmid.d 
 |-  .- = ( dist ` G )
3 symquadmid.i 
 |-  I = ( Itv ` G )
4 symquadmid.l 
 |-  L = ( LineG ` G )
5 symquadmid.m 
 |-  M = ( midG ` G )
6 symquadmid.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 ) ) }
7 symquadmid.g 
 |-  ( ph -> G e. TarskiG )
8 symquadmid.x 
 |-  ( ph -> X e. P )
9 symquadmid.y 
 |-  ( ph -> Y e. P )
10 symquadmid.z 
 |-  ( ph -> Z e. P )
11 symquadmid.w 
 |-  ( ph -> W e. P )
12 symquadmid.2 
 |-  ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
13 symquadmid.3 
 |-  ( ph -> Y =/= W )
14 symquadmid.4 
 |-  ( ph -> ( X .- Y ) = ( Z .- W ) )
15 symquadmid.5 
 |-  ( ph -> ( Y .- Z ) = ( W .- X ) )
16 symquadmid.6 
 |-  ( ph -> Y O W )
17 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
18 7 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> G e. TarskiG )
19 eqid 
 |-  ( ( pInvG ` G ) ` t ) = ( ( pInvG ` G ) ` t )
20 8 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> X e. P )
21 9 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> Y e. P )
22 10 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> Z e. P )
23 11 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> W e. P )
24 1 3 4 7 8 9 10 12 ncolne2 
 |-  ( ph -> X =/= Z )
25 1 3 4 7 8 10 24 tgelrnln 
 |-  ( ph -> ( X L Z ) e. ran L )
26 25 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X L Z ) e. ran L )
27 simplr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> t e. ( X L Z ) )
28 1 4 3 18 26 27 tglnpt 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> t e. P )
29 12 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
30 13 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> Y =/= W )
31 14 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X .- Y ) = ( Z .- W ) )
32 15 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Y .- Z ) = ( W .- X ) )
33 27 orcd 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( t e. ( X L Z ) \/ X = Z ) )
34 simpr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> t e. ( Y I W ) )
35 1 3 4 18 21 23 28 30 34 btwnlng1 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> t e. ( Y L W ) )
36 35 orcd 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( t e. ( Y L W ) \/ Y = W ) )
37 1 2 3 4 17 18 19 20 21 22 23 28 29 30 31 32 33 36 symquadlem 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> X = ( ( ( pInvG ` G ) ` t ) ` Z ) )
38 1 4 3 7 9 10 8 12 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
39 38 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> G TarskiGDim>= 2 )
40 1 2 3 18 39 22 20 17 28 ismidb 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X = ( ( ( pInvG ` G ) ` t ) ` Z ) <-> ( Z ( midG ` G ) X ) = t ) )
41 37 40 mpbid 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Z ( midG ` G ) X ) = t )
42 1 2 3 18 39 20 22 midcom 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X ( midG ` G ) Z ) = ( Z ( midG ` G ) X ) )
43 1 2 3 18 39 21 23 midcom 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Y ( midG ` G ) W ) = ( W ( midG ` G ) Y ) )
44 15 eqcomd 
 |-  ( ph -> ( W .- X ) = ( Y .- Z ) )
45 1 2 3 7 11 8 9 10 44 tgcgrcomlr 
 |-  ( ph -> ( X .- W ) = ( Z .- Y ) )
46 45 eqcomd 
 |-  ( ph -> ( Z .- Y ) = ( X .- W ) )
47 46 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Z .- Y ) = ( X .- W ) )
48 1 2 3 7 8 9 10 11 14 tgcgrcomlr 
 |-  ( ph -> ( Y .- X ) = ( W .- Z ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Y .- X ) = ( W .- Z ) )
50 1 4 3 7 9 10 8 12 ncolrot2 
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
51 1 4 3 7 8 9 10 50 ncolcom 
 |-  ( ph -> -. ( Z e. ( Y L X ) \/ Y = X ) )
52 51 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> -. ( Z e. ( Y L X ) \/ Y = X ) )
53 1 3 4 7 8 10 24 tglinecom 
 |-  ( ph -> ( X L Z ) = ( Z L X ) )
54 53 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X L Z ) = ( Z L X ) )
55 27 54 eleqtrd 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> t e. ( Z L X ) )
56 1 2 4 18 22 21 20 23 47 49 52 30 55 35 symquadprlnglem 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> -. ( W e. ( X L Y ) \/ X = Y ) )
57 1 4 3 18 20 21 23 56 ncolcom 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> -. ( W e. ( Y L X ) \/ Y = X ) )
58 1 4 3 18 21 20 23 57 ncolrot1 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> -. ( Y e. ( X L W ) \/ X = W ) )
59 24 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> X =/= Z )
60 45 ad2antrr 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X .- W ) = ( Z .- Y ) )
61 1 2 3 4 17 18 19 21 20 23 22 28 58 59 49 60 36 33 symquadlem 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> Y = ( ( ( pInvG ` G ) ` t ) ` W ) )
62 1 2 3 18 39 23 21 17 28 ismidb 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Y = ( ( ( pInvG ` G ) ` t ) ` W ) <-> ( W ( midG ` G ) Y ) = t ) )
63 61 62 mpbid 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( W ( midG ` G ) Y ) = t )
64 43 63 eqtrd 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( Y ( midG ` G ) W ) = t )
65 41 42 64 3eqtr4d 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X ( midG ` G ) Z ) = ( Y ( midG ` G ) W ) )
66 5 oveqi 
 |-  ( X M Z ) = ( X ( midG ` G ) Z )
67 5 oveqi 
 |-  ( Y M W ) = ( Y ( midG ` G ) W )
68 65 66 67 3eqtr4g 
 |-  ( ( ( ph /\ t e. ( X L Z ) ) /\ t e. ( Y I W ) ) -> ( X M Z ) = ( Y M W ) )
69 1 2 3 6 9 11 islnopp 
 |-  ( ph -> ( Y O W <-> ( ( -. Y e. ( X L Z ) /\ -. W e. ( X L Z ) ) /\ E. t e. ( X L Z ) t e. ( Y I W ) ) ) )
70 16 69 mpbid 
 |-  ( ph -> ( ( -. Y e. ( X L Z ) /\ -. W e. ( X L Z ) ) /\ E. t e. ( X L Z ) t e. ( Y I W ) ) )
71 70 simprd 
 |-  ( ph -> E. t e. ( X L Z ) t e. ( Y I W ) )
72 68 71 r19.29a 
 |-  ( ph -> ( X M Z ) = ( Y M W ) )