Metamath Proof Explorer

Theorem prlngsymquad

Description: All parallelograms are symmetric quadrilaterals. First part of Theorem 12.19 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 ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
prlngsymquad.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
prlngsymquad.3 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
prlngsymquad.4 ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
Assertion prlngsymquad ( 𝜑 → ( ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )

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 prlngsymquad.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
12 prlngsymquad.3 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
13 prlngsymquad.4 ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
15 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
16 1 3 15 5 8 9 7 11 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
17 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
18 1 2 15 5 16 7 9 midcl ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ 𝑃 )
19 1 2 15 5 16 7 9 17 18 ismidb ⊢ ( 𝜑 → ( 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) ↔ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) )
20 14 19 mpbird ⊢ ( 𝜑 → 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) )
21 20 eqcomd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) = 𝑍 )
22 21 oveq1d ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) )
23 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
24 1 2 15 3 17 5 18 23 7 8 miriso ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) = ( 𝑋 − 𝑌 ) )
25 eqid ⊢ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 25 prlngsymquadlem ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) = 𝑊 )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) = ( 𝑍 − 𝑊 ) )
28 22 24 27 3eqtr3d ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
29 1 2 15 3 17 5 18 23 7 21 mircom ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) = 𝑋 )
30 29 oveq2d ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) − 𝑋 ) )
31 1 2 15 3 17 5 18 23 8 9 miriso ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) ) = ( 𝑌 − 𝑍 ) )
32 26 oveq1d ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) − 𝑋 ) = ( 𝑊 − 𝑋 ) )
33 30 31 32 3eqtr3d ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
34 28 33 jca ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )