Metamath Proof Explorer

Theorem symquadlem

Description: Lemma of the symetrial quadrilateral. The diagonals of quadrilaterals with congruent opposing sides intersect at their middle point. In Euclidean geometry, such quadrilaterals are called parallelograms, as opposing sides are parallel. However, this is not necessarily true in the case of absolute geometry. Lemma 7.21 of Schwabhauser p. 52. (Contributed by Thierry Arnoux, 6-Aug-2019)

Ref Expression
Hypotheses mirval.p 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
symquadlem.m 
|- M = ( S ` X )
symquadlem.a 
|- ( ph -> A e. P )
symquadlem.b 
|- ( ph -> B e. P )
symquadlem.c 
|- ( ph -> C e. P )
symquadlem.d 
|- ( ph -> D e. P )
symquadlem.x 
|- ( ph -> X e. P )
symquadlem.1 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
symquadlem.2 
|- ( ph -> B =/= D )
symquadlem.3 
|- ( ph -> ( A .- B ) = ( C .- D ) )
symquadlem.4 
|- ( ph -> ( B .- C ) = ( D .- A ) )
symquadlem.5 
|- ( ph -> ( X e. ( A L C ) \/ A = C ) )
symquadlem.6 
|- ( ph -> ( X e. ( B L D ) \/ B = D ) )
Assertion symquadlem 
|- ( ph -> A = ( M ` C ) )

Proof

Step Hyp Ref Expression
1 mirval.p 
 |-  P = ( Base ` G )
2 mirval.d 
 |-  .- = ( dist ` G )
3 mirval.i 
 |-  I = ( Itv ` G )
4 mirval.l 
 |-  L = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 symquadlem.m 
 |-  M = ( S ` X )
8 symquadlem.a 
 |-  ( ph -> A e. P )
9 symquadlem.b 
 |-  ( ph -> B e. P )
10 symquadlem.c 
 |-  ( ph -> C e. P )
11 symquadlem.d 
 |-  ( ph -> D e. P )
12 symquadlem.x 
 |-  ( ph -> X e. P )
13 symquadlem.1 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
14 symquadlem.2 
 |-  ( ph -> B =/= D )
15 symquadlem.3 
 |-  ( ph -> ( A .- B ) = ( C .- D ) )
16 symquadlem.4 
 |-  ( ph -> ( B .- C ) = ( D .- A ) )
17 symquadlem.5 
 |-  ( ph -> ( X e. ( A L C ) \/ A = C ) )
18 symquadlem.6 
 |-  ( ph -> ( X e. ( B L D ) \/ B = D ) )
19 1 2 3 6 9 8 tgbtwntriv2 
 |-  ( ph -> A e. ( B I A ) )
20 1 4 3 6 9 8 8 19 btwncolg1 
 |-  ( ph -> ( A e. ( B L A ) \/ B = A ) )
21 20 adantr 
 |-  ( ( ph /\ A = C ) -> ( A e. ( B L A ) \/ B = A ) )
22 simpr 
 |-  ( ( ph /\ A = C ) -> A = C )
23 22 oveq2d 
 |-  ( ( ph /\ A = C ) -> ( B L A ) = ( B L C ) )
24 23 eleq2d 
 |-  ( ( ph /\ A = C ) -> ( A e. ( B L A ) <-> A e. ( B L C ) ) )
25 22 eqeq2d 
 |-  ( ( ph /\ A = C ) -> ( B = A <-> B = C ) )
26 24 25 orbi12d 
 |-  ( ( ph /\ A = C ) -> ( ( A e. ( B L A ) \/ B = A ) <-> ( A e. ( B L C ) \/ B = C ) ) )
27 21 26 mpbid 
 |-  ( ( ph /\ A = C ) -> ( A e. ( B L C ) \/ B = C ) )
28 13 27 mtand 
 |-  ( ph -> -. A = C )
29 28 neqned 
 |-  ( ph -> A =/= C )
30 29 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> A =/= C )
31 30 necomd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> C =/= A )
32 31 neneqd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> -. C = A )
33 6 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> G e. TarskiG )
34 10 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> C e. P )
35 8 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> A e. P )
36 12 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> X e. P )
37 17 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X e. ( A L C ) \/ A = C ) )
38 1 4 3 33 35 34 36 37 colcom 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X e. ( C L A ) \/ C = A ) )
39 9 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> B e. P )
40 11 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> D e. P )
41 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
42 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> x e. P )
43 1 4 3 6 9 11 12 18 colrot2 
 |-  ( ph -> ( D e. ( X L B ) \/ X = B ) )
44 1 4 3 6 12 9 11 43 colcom 
 |-  ( ph -> ( D e. ( B L X ) \/ B = X ) )
45 44 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( D e. ( B L X ) \/ B = X ) )
46 simpr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> <" B D X "> ( cgrG ` G ) <" D B x "> )
47 16 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( B .- C ) = ( D .- A ) )
48 1 2 3 6 8 9 10 11 15 tgcgrcomlr 
 |-  ( ph -> ( B .- A ) = ( D .- C ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( B .- A ) = ( D .- C ) )
50 49 eqcomd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( D .- C ) = ( B .- A ) )
51 14 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> B =/= D )
52 1 4 3 33 39 40 36 41 40 39 2 34 42 35 45 46 47 50 51 tgfscgr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X .- C ) = ( x .- A ) )
53 1 4 3 6 9 10 8 13 ncolcom 
 |-  ( ph -> -. ( A e. ( C L B ) \/ C = B ) )
54 53 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> -. ( A e. ( C L B ) \/ C = B ) )
55 17 orcomd 
 |-  ( ph -> ( A = C \/ X e. ( A L C ) ) )
56 55 ord 
 |-  ( ph -> ( -. A = C -> X e. ( A L C ) ) )
57 28 56 mpd 
 |-  ( ph -> X e. ( A L C ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> X e. ( A L C ) )
59 28 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> -. A = C )
60 47 eqcomd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( D .- A ) = ( B .- C ) )
61 1 4 3 33 39 40 36 41 40 39 2 35 42 34 45 46 49 60 51 tgfscgr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X .- A ) = ( x .- C ) )
62 1 2 3 33 36 35 42 34 61 tgcgrcomlr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( A .- X ) = ( C .- x ) )
63 1 2 3 33 34 35 axtgcgrrflx 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( C .- A ) = ( A .- C ) )
64 1 2 41 33 35 36 34 34 42 35 62 52 63 trgcgr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> <" A X C "> ( cgrG ` G ) <" C x A "> )
65 1 4 3 33 35 36 34 41 34 42 35 37 64 lnxfr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( x e. ( C L A ) \/ C = A ) )
66 1 4 3 33 34 35 42 65 colcom 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( x e. ( A L C ) \/ A = C ) )
67 66 orcomd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( A = C \/ x e. ( A L C ) ) )
68 67 ord 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( -. A = C -> x e. ( A L C ) ) )
69 59 68 mpd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> x e. ( A L C ) )
70 14 neneqd 
 |-  ( ph -> -. B = D )
71 18 orcomd 
 |-  ( ph -> ( B = D \/ X e. ( B L D ) ) )
72 71 ord 
 |-  ( ph -> ( -. B = D -> X e. ( B L D ) ) )
73 70 72 mpd 
 |-  ( ph -> X e. ( B L D ) )
74 73 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> X e. ( B L D ) )
75 70 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> -. B = D )
76 18 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X e. ( B L D ) \/ B = D ) )
77 1 2 3 41 33 39 40 36 40 39 42 46 cgr3swap23 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> <" B X D "> ( cgrG ` G ) <" D x B "> )
78 1 4 3 33 39 36 40 41 40 42 39 76 77 lnxfr 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( x e. ( D L B ) \/ D = B ) )
79 1 4 3 33 40 39 42 78 colcom 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( x e. ( B L D ) \/ B = D ) )
80 79 orcomd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( B = D \/ x e. ( B L D ) ) )
81 80 ord 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( -. B = D -> x e. ( B L D ) ) )
82 75 81 mpd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> x e. ( B L D ) )
83 1 3 4 33 35 34 39 40 54 58 69 74 82 tglineinteq 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> X = x )
84 83 oveq1d 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X .- A ) = ( x .- A ) )
85 52 84 eqtr4d 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( X .- C ) = ( X .- A ) )
86 1 2 3 4 5 33 7 34 35 36 38 85 colmid 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( A = ( M ` C ) \/ C = A ) )
87 86 orcomd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( C = A \/ A = ( M ` C ) ) )
88 87 ord 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> ( -. C = A -> A = ( M ` C ) ) )
89 32 88 mpd 
 |-  ( ( ( ph /\ x e. P ) /\ <" B D X "> ( cgrG ` G ) <" D B x "> ) -> A = ( M ` C ) )
90 1 2 3 6 9 11 axtgcgrrflx 
 |-  ( ph -> ( B .- D ) = ( D .- B ) )
91 1 4 3 6 9 11 12 41 11 9 2 44 90 lnext 
 |-  ( ph -> E. x e. P <" B D X "> ( cgrG ` G ) <" D B x "> )
92 89 91 r19.29a 
 |-  ( ph -> A = ( M ` C ) )