Metamath Proof Explorer


Theorem lncgr

Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 28-Apr-2019)

Ref Expression
Hypotheses tglngval.p 𝑃 = ( Base ‘ 𝐺 )
tglngval.l 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ( 𝜑𝐺 ∈ TarskiG )
tglngval.x ( 𝜑𝑋𝑃 )
tglngval.y ( 𝜑𝑌𝑃 )
tgcolg.z ( 𝜑𝑍𝑃 )
lnxfr.r = ( cgrG ‘ 𝐺 )
lnxfr.a ( 𝜑𝐴𝑃 )
lnxfr.b ( 𝜑𝐵𝑃 )
lnxfr.d = ( dist ‘ 𝐺 )
lncgr.1 ( 𝜑𝑋𝑌 )
lncgr.2 ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
lncgr.3 ( 𝜑 → ( 𝑋 𝐴 ) = ( 𝑋 𝐵 ) )
lncgr.4 ( 𝜑 → ( 𝑌 𝐴 ) = ( 𝑌 𝐵 ) )
Assertion lncgr ( 𝜑 → ( 𝑍 𝐴 ) = ( 𝑍 𝐵 ) )

Proof

Step Hyp Ref Expression
1 tglngval.p 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ( 𝜑𝐺 ∈ TarskiG )
5 tglngval.x ( 𝜑𝑋𝑃 )
6 tglngval.y ( 𝜑𝑌𝑃 )
7 tgcolg.z ( 𝜑𝑍𝑃 )
8 lnxfr.r = ( cgrG ‘ 𝐺 )
9 lnxfr.a ( 𝜑𝐴𝑃 )
10 lnxfr.b ( 𝜑𝐵𝑃 )
11 lnxfr.d = ( dist ‘ 𝐺 )
12 lncgr.1 ( 𝜑𝑋𝑌 )
13 lncgr.2 ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
14 lncgr.3 ( 𝜑 → ( 𝑋 𝐴 ) = ( 𝑋 𝐵 ) )
15 lncgr.4 ( 𝜑 → ( 𝑌 𝐴 ) = ( 𝑌 𝐵 ) )
16 1 11 3 8 4 5 6 7 cgr3id ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
17 1 2 3 4 5 6 7 8 5 6 11 9 7 10 13 16 14 15 12 tgfscgr ( 𝜑 → ( 𝑍 𝐴 ) = ( 𝑍 𝐵 ) )