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 | ⊢ ( 𝜑 → ( 𝑍 − 𝐴 ) = ( 𝑍 − 𝐵 ) ) |
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 | ⊢ ( 𝜑 → ( 𝑍 − 𝐴 ) = ( 𝑍 − 𝐵 ) ) |