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	$⊢ \underset{˙}{-} = dist (G)$
	symquadmid.i	$⊢ I = Itv (G)$
	symquadmid.l	$⊢ L = {Line}_{𝒢} (G)$
	symquadmid.m	$⊢ M = {mid}_{𝒢} (G)$
	symquadmid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\}$
	symquadmid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	symquadmid.x	$⊢ φ \to X \in P$
	symquadmid.y	$⊢ φ \to Y \in P$
	symquadmid.z	$⊢ φ \to Z \in P$
	symquadmid.w	$⊢ φ \to W \in P$
	symquadmid.2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
	symquadmid.3	$⊢ φ \to Y \neq W$
	symquadmid.4	$⊢ φ \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
	symquadmid.5	$⊢ φ \to Y \underset{˙}{-} Z = W \underset{˙}{-} X$
	symquadmid.6	$⊢ φ \to Y O W$
Assertion	symquadmid	$⊢ φ \to X M Z = Y M W$

Proof

Step	Hyp	Ref	Expression
1		symquadmid.p	$⊢ P = {Base}_{G}$
2		symquadmid.d	$⊢ \underset{˙}{-} = dist (G)$
3		symquadmid.i	$⊢ I = Itv (G)$
4		symquadmid.l	$⊢ L = {Line}_{𝒢} (G)$
5		symquadmid.m	$⊢ M = {mid}_{𝒢} (G)$
6		symquadmid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\}$
7		symquadmid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		symquadmid.x	$⊢ φ \to X \in P$
9		symquadmid.y	$⊢ φ \to Y \in P$
10		symquadmid.z	$⊢ φ \to Z \in P$
11		symquadmid.w	$⊢ φ \to W \in P$
12		symquadmid.2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
13		symquadmid.3	$⊢ φ \to Y \neq W$
14		symquadmid.4	$⊢ φ \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
15		symquadmid.5	$⊢ φ \to Y \underset{˙}{-} Z = W \underset{˙}{-} X$
16		symquadmid.6	$⊢ φ \to Y O W$
17		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
18	7	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to G \in 𝒢_{Tarski}$
19		eqid	$⊢ {pInv}_{𝒢} (G) (t) = {pInv}_{𝒢} (G) (t)$
20	8	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X \in P$
21	9	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y \in P$
22	10	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Z \in P$
23	11	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to W \in P$
24	1 3 4 7 8 9 10 12	ncolne2	$⊢ φ \to X \neq Z$
25	1 3 4 7 8 10 24	tgelrnln	$⊢ φ \to X L Z \in ran L$
26	25	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X L Z \in ran L$
27		simplr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to t \in (X L Z)$
28	1 4 3 18 26 27	tglnpt	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to t \in P$
29	12	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to \neg (X \in (Y L Z) \lor Y = Z)$
30	13	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y \neq W$
31	14	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
32	15	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y \underset{˙}{-} Z = W \underset{˙}{-} X$
33	27	orcd	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to (t \in (X L Z) \lor X = Z)$
34		simpr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to t \in (Y I W)$
35	1 3 4 18 21 23 28 30 34	btwnlng1	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to t \in (Y L W)$
36	35	orcd	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to (t \in (Y L W) \lor Y = W)$
37	1 2 3 4 17 18 19 20 21 22 23 28 29 30 31 32 33 36	symquadlem	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X = {pInv}_{𝒢} (G) (t) (Z)$
38	1 4 3 7 9 10 8 12	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
39	38	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to G {Dim}_{𝒢} \geq 2$
40	1 2 3 18 39 22 20 17 28	ismidb	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to (X = {pInv}_{𝒢} (G) (t) (Z) \leftrightarrow Z {mid}_{𝒢} (G) X = t)$
41	37 40	mpbid	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Z {mid}_{𝒢} (G) X = t$
42	1 2 3 18 39 20 22	midcom	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X {mid}_{𝒢} (G) Z = Z {mid}_{𝒢} (G) X$
43	1 2 3 18 39 21 23	midcom	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y {mid}_{𝒢} (G) W = W {mid}_{𝒢} (G) Y$
44	15	eqcomd	$⊢ φ \to W \underset{˙}{-} X = Y \underset{˙}{-} Z$
45	1 2 3 7 11 8 9 10 44	tgcgrcomlr	$⊢ φ \to X \underset{˙}{-} W = Z \underset{˙}{-} Y$
46	45	eqcomd	$⊢ φ \to Z \underset{˙}{-} Y = X \underset{˙}{-} W$
47	46	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Z \underset{˙}{-} Y = X \underset{˙}{-} W$
48	1 2 3 7 8 9 10 11 14	tgcgrcomlr	$⊢ φ \to Y \underset{˙}{-} X = W \underset{˙}{-} Z$
49	48	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y \underset{˙}{-} X = W \underset{˙}{-} Z$
50	1 4 3 7 9 10 8 12	ncolrot2	$⊢ φ \to \neg (Z \in (X L Y) \lor X = Y)$
51	1 4 3 7 8 9 10 50	ncolcom	$⊢ φ \to \neg (Z \in (Y L X) \lor Y = X)$
52	51	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to \neg (Z \in (Y L X) \lor Y = X)$
53	1 3 4 7 8 10 24	tglinecom	$⊢ φ \to X L Z = Z L X$
54	53	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X L Z = Z L X$
55	27 54	eleqtrd	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to t \in (Z L X)$
56	1 2 4 18 22 21 20 23 47 49 52 30 55 35	symquadprlnglem	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to \neg (W \in (X L Y) \lor X = Y)$
57	1 4 3 18 20 21 23 56	ncolcom	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to \neg (W \in (Y L X) \lor Y = X)$
58	1 4 3 18 21 20 23 57	ncolrot1	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to \neg (Y \in (X L W) \lor X = W)$
59	24	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X \neq Z$
60	45	ad2antrr	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X \underset{˙}{-} W = Z \underset{˙}{-} Y$
61	1 2 3 4 17 18 19 21 20 23 22 28 58 59 49 60 36 33	symquadlem	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y = {pInv}_{𝒢} (G) (t) (W)$
62	1 2 3 18 39 23 21 17 28	ismidb	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to (Y = {pInv}_{𝒢} (G) (t) (W) \leftrightarrow W {mid}_{𝒢} (G) Y = t)$
63	61 62	mpbid	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to W {mid}_{𝒢} (G) Y = t$
64	43 63	eqtrd	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to Y {mid}_{𝒢} (G) W = t$
65	41 42 64	3eqtr4d	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X {mid}_{𝒢} (G) Z = Y {mid}_{𝒢} (G) W$
66	5	oveqi	$⊢ X M Z = X {mid}_{𝒢} (G) Z$
67	5	oveqi	$⊢ Y M W = Y {mid}_{𝒢} (G) W$
68	65 66 67	3eqtr4g	$⊢ ((φ \land t \in (X L Z)) \land t \in (Y I W)) \to X M Z = Y M W$
69	1 2 3 6 9 11	islnopp	$⊢ φ \to (Y O W \leftrightarrow ((\neg Y \in (X L Z) \land \neg W \in (X L Z)) \land \exists t \in (X L Z) t \in (Y I W)))$
70	16 69	mpbid	$⊢ φ \to ((\neg Y \in (X L Z) \land \neg W \in (X L Z)) \land \exists t \in (X L Z) t \in (Y I W))$
71	70	simprd	$⊢ φ \to \exists t \in (X L Z) t \in (Y I W)$
72	68 71	r19.29a	$⊢ φ \to X M Z = Y M W$

Metamath Proof Explorer

Theorem symquadmid

Proof