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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
symquadmid.d ⊢ − = ( dist ‘ 𝐺 )
symquadmid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
symquadmid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
symquadmid.m ⊢ 𝑀 = ( midG ‘ 𝐺 )
symquadmid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
symquadmid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
symquadmid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
symquadmid.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
symquadmid.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
symquadmid.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
symquadmid.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
symquadmid.3 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
symquadmid.4 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
symquadmid.5 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
symquadmid.6 ⊢ ( 𝜑 → 𝑌 𝑂 𝑊 )
Assertion symquadmid ( 𝜑 → ( 𝑋 𝑀 𝑍 ) = ( 𝑌 𝑀 𝑊 ) )

Proof

Step Hyp Ref Expression
1 symquadmid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 symquadmid.d ⊢ − = ( dist ‘ 𝐺 )
3 symquadmid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 symquadmid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 symquadmid.m ⊢ 𝑀 = ( midG ‘ 𝐺 )
6 symquadmid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
7 symquadmid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 symquadmid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9 symquadmid.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10 symquadmid.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
11 symquadmid.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
12 symquadmid.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
13 symquadmid.3 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
14 symquadmid.4 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
15 symquadmid.5 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
16 symquadmid.6 ⊢ ( 𝜑 → 𝑌 𝑂 𝑊 )
17 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
18 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝐺 ∈ TarskiG )
19 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 )
20 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑋 ∈ 𝑃 )
21 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑌 ∈ 𝑃 )
22 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑍 ∈ 𝑃 )
23 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑊 ∈ 𝑃 )
24 1 3 4 7 8 9 10 12 ncolne2 ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
25 1 3 4 7 8 10 24 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
27 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) )
28 1 4 3 18 26 27 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑡 ∈ 𝑃 )
29 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
30 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑌 ≠ 𝑊 )
31 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
32 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
33 27 orcd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) )
35 1 3 4 18 21 23 28 30 34 btwnlng1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑡 ∈ ( 𝑌 𝐿 𝑊 ) )
36 35 orcd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑡 ∈ ( 𝑌 𝐿 𝑊 ) ∨ 𝑌 = 𝑊 ) )
37 1 2 3 4 17 18 19 20 21 22 23 28 29 30 31 32 33 36 symquadlem ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑋 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑍 ) )
38 1 4 3 7 9 10 8 12 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝐺 DimTarskiG≥ 2 )
40 1 2 3 18 39 22 20 17 28 ismidb ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑍 ) ↔ ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) = 𝑡 ) )
41 37 40 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) = 𝑡 )
42 1 2 3 18 39 20 22 midcom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) )
43 1 2 3 18 39 21 23 midcom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = ( 𝑊 ( midG ‘ 𝐺 ) 𝑌 ) )
44 15 eqcomd ⊢ ( 𝜑 → ( 𝑊 − 𝑋 ) = ( 𝑌 − 𝑍 ) )
45 1 2 3 7 11 8 9 10 44 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑋 − 𝑊 ) = ( 𝑍 − 𝑌 ) )
46 45 eqcomd ⊢ ( 𝜑 → ( 𝑍 − 𝑌 ) = ( 𝑋 − 𝑊 ) )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑍 − 𝑌 ) = ( 𝑋 − 𝑊 ) )
48 1 2 3 7 8 9 10 11 14 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) = ( 𝑊 − 𝑍 ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑌 − 𝑋 ) = ( 𝑊 − 𝑍 ) )
50 1 4 3 7 9 10 8 12 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
51 1 4 3 7 8 9 10 50 ncolcom ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ¬ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )
53 1 3 4 7 8 10 24 tglinecom ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
55 27 54 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑡 ∈ ( 𝑍 𝐿 𝑋 ) )
56 1 2 4 18 22 21 20 23 47 49 52 30 55 35 symquadprlnglem ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ¬ ( 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
57 1 4 3 18 20 21 23 56 ncolcom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ¬ ( 𝑊 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )
58 1 4 3 18 21 20 23 57 ncolrot1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ¬ ( 𝑌 ∈ ( 𝑋 𝐿 𝑊 ) ∨ 𝑋 = 𝑊 ) )
59 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑋 ≠ 𝑍 )
60 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 − 𝑊 ) = ( 𝑍 − 𝑌 ) )
61 1 2 3 4 17 18 19 21 20 23 22 28 58 59 49 60 36 33 symquadlem ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → 𝑌 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑊 ) )
62 1 2 3 18 39 23 21 17 28 ismidb ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑌 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑊 ) ↔ ( 𝑊 ( midG ‘ 𝐺 ) 𝑌 ) = 𝑡 ) )
63 61 62 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑊 ( midG ‘ 𝐺 ) 𝑌 ) = 𝑡 )
64 43 63 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = 𝑡 )
65 41 42 64 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) )
66 5 oveqi ⊢ ( 𝑋 𝑀 𝑍 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 )
67 5 oveqi ⊢ ( 𝑌 𝑀 𝑊 ) = ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 )
68 65 66 67 3eqtr4g ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) → ( 𝑋 𝑀 𝑍 ) = ( 𝑌 𝑀 𝑊 ) )
69 1 2 3 6 9 11 islnopp ⊢ ( 𝜑 → ( 𝑌 𝑂 𝑊 ↔ ( ( ¬ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∧ ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) ) )
70 16 69 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∧ ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) ) )
71 70 simprd ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑌 𝐼 𝑊 ) )
72 68 71 r19.29a ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑍 ) = ( 𝑌 𝑀 𝑊 ) )