Database
ELEMENTARY GEOMETRY
Tarskian Geometry
Congruence
tgcgrcoml
Metamath Proof Explorer
Description: Congruence commutes on the LHS. Variant of Theorem 2.5 of
Schwabhauser p. 27, but in a convenient form for a common case.
(Contributed by David A. Wheeler , 29-Jun-2020)
Ref
Expression
Hypotheses
tkgeom.p
⊢ 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d
⊢ − = ( dist ‘ 𝐺 )
tkgeom.i
⊢ 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g
⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgcgrcomr.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgcgrcomr.b
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgcgrcomr.c
⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgcgrcomr.d
⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgcgrcomr.6
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
Assertion
tgcgrcoml
⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐶 − 𝐷 ) )
Proof
Step
Hyp
Ref
Expression
1
tkgeom.p
⊢ 𝑃 = ( Base ‘ 𝐺 )
2
tkgeom.d
⊢ − = ( dist ‘ 𝐺 )
3
tkgeom.i
⊢ 𝐼 = ( Itv ‘ 𝐺 )
4
tkgeom.g
⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5
tgcgrcomr.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6
tgcgrcomr.b
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7
tgcgrcomr.c
⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8
tgcgrcomr.d
⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9
tgcgrcomr.6
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
10
1 2 3 4 5 6
axtgcgrrflx
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
11
10 9
eqtr3d
⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐶 − 𝐷 ) )