symquadlem

Description: Lemma of the symmetrical 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	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	symquadlem.m	$⊢ M = S (X)$
	symquadlem.a	$⊢ φ \to A \in P$
	symquadlem.b	$⊢ φ \to B \in P$
	symquadlem.c	$⊢ φ \to C \in P$
	symquadlem.d	$⊢ φ \to D \in P$
	symquadlem.x	$⊢ φ \to X \in P$
	symquadlem.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	symquadlem.2	$⊢ φ \to B \neq D$
	symquadlem.3	$⊢ φ \to A \underset{˙}{-} B = C \underset{˙}{-} D$
	symquadlem.4	$⊢ φ \to B \underset{˙}{-} C = D \underset{˙}{-} A$
	symquadlem.5	$⊢ φ \to (X \in (A L C) \lor A = C)$
	symquadlem.6	$⊢ φ \to (X \in (B L D) \lor B = D)$
Assertion	symquadlem	$⊢ φ \to A = M (C)$

Proof

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

Metamath Proof Explorer

Theorem symquadlem

Proof