Metamath Proof Explorer

Theorem symquadprlng

Description: Symmetrical quadrilaterals are parallelograms. Theorem 12.18 of Schwabhauser p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses symquadprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
symquadprlng.d ⊢ − = ( dist ‘ 𝐺 )
symquadprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
symquadprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
symquadprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
symquadprlng.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
symquadprlng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
symquadprlng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
symquadprlng.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
symquadprlng.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
symquadprlng.2 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
symquadprlng.3 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
symquadprlng.4 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
symquadprlng.5 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
symquadprlng.6 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑋 𝐿 𝑍 ) )
symquadprlng.7 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑌 𝐿 𝑊 ) )
Assertion symquadprlng ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 symquadprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 symquadprlng.d ⊢ − = ( dist ‘ 𝐺 )
3 symquadprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 symquadprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
5 symquadprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 symquadprlng.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
7 symquadprlng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
8 symquadprlng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
9 symquadprlng.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
10 symquadprlng.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 symquadprlng.2 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
12 symquadprlng.3 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
13 symquadprlng.4 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
14 symquadprlng.5 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
15 symquadprlng.6 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑋 𝐿 𝑍 ) )
16 symquadprlng.7 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑌 𝐿 𝑊 ) )
17 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
18 eqid ⊢ ( midG ‘ 𝐺 ) = ( midG ‘ 𝐺 )
19 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
20 1 3 19 5 8 9 7 13 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
21 20 orsild ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
22 9 21 eldifd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
23 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
24 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 )
25 1 19 3 5 8 10 14 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑊 ) ∈ ran 𝐿 )
26 1 3 19 5 25 16 tglnpt ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
27 15 orcd ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
28 16 orcd ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑌 𝐿 𝑊 ) ∨ 𝑌 = 𝑊 ) )
29 1 2 19 3 23 5 24 7 8 9 10 26 13 14 11 12 27 28 symquadlem ⊢ ( 𝜑 → 𝑋 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑍 ) )
30 1 3 19 5 8 9 7 13 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
31 1 2 19 5 30 9 7 23 26 ismidb ⊢ ( 𝜑 → ( 𝑋 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑍 ) ↔ ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) = 𝑇 ) )
32 29 31 mpbid ⊢ ( 𝜑 → ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) = 𝑇 )
33 1 2 19 5 30 7 9 midcom ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) )
34 1 2 3 5 7 8 9 10 11 12 13 14 15 16 symquadprlnglem ⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
35 1 3 19 5 7 9 15 tglngne ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
36 35 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑋 )
37 1 2 19 5 7 8 9 10 11 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) = ( 𝑊 − 𝑍 ) )
38 37 eqcomd ⊢ ( 𝜑 → ( 𝑊 − 𝑍 ) = ( 𝑌 − 𝑋 ) )
39 1 2 19 5 8 9 10 7 12 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑍 − 𝑌 ) = ( 𝑋 − 𝑊 ) )
40 1 3 19 5 8 10 26 28 colcom ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑊 𝐿 𝑌 ) ∨ 𝑊 = 𝑌 ) )
41 1 3 19 5 7 9 26 27 colcom ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑍 𝐿 𝑋 ) ∨ 𝑍 = 𝑋 ) )
42 1 2 19 3 23 5 24 10 9 8 7 26 34 36 38 39 40 41 symquadlem ⊢ ( 𝜑 → 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑌 ) )
43 1 2 19 5 30 8 10 23 26 ismidb ⊢ ( 𝜑 → ( 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑌 ) ↔ ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = 𝑇 ) )
44 42 43 mpbid ⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = 𝑇 )
45 32 33 44 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) )
46 1 19 3 5 7 8 9 13 ncolne1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
47 1 3 17 4 18 5 6 7 8 22 10 45 46 prlngmid2 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
48 34 orsild ⊢ ( 𝜑 → ¬ 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) )
49 34 orsird ⊢ ( 𝜑 → ¬ 𝑍 = 𝑌 )
50 49 neqned ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
51 1 19 3 5 9 8 50 tglinecom ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑍 ) )
52 48 51 neleqtrd ⊢ ( 𝜑 → ¬ 𝑊 ∈ ( 𝑌 𝐿 𝑍 ) )
53 10 52 eldifd ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) )
54 44 32 eqtr4d ⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) )
55 50 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
56 1 3 17 4 18 5 6 8 9 53 7 54 55 prlngmid2 ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
57 47 56 jca ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ) )