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 P=BaseG
tglngval.l L=Line𝒢G
tglngval.i I=ItvG
tglngval.g φG𝒢Tarski
tglngval.x φXP
tglngval.y φYP
tgcolg.z φZP
lnxfr.r ˙=𝒢G
lnxfr.a φAP
lnxfr.b φBP
lnxfr.d -˙=distG
lncgr.1 φXY
lncgr.2 φYXLZX=Z
lncgr.3 φX-˙A=X-˙B
lncgr.4 φY-˙A=Y-˙B
Assertion lncgr φZ-˙A=Z-˙B

Proof

Step Hyp Ref Expression
1 tglngval.p P=BaseG
2 tglngval.l L=Line𝒢G
3 tglngval.i I=ItvG
4 tglngval.g φG𝒢Tarski
5 tglngval.x φXP
6 tglngval.y φYP
7 tgcolg.z φZP
8 lnxfr.r ˙=𝒢G
9 lnxfr.a φAP
10 lnxfr.b φBP
11 lnxfr.d -˙=distG
12 lncgr.1 φXY
13 lncgr.2 φYXLZX=Z
14 lncgr.3 φX-˙A=X-˙B
15 lncgr.4 φY-˙A=Y-˙B
16 1 11 3 8 4 5 6 7 cgr3id φ⟨“XYZ”⟩˙⟨“XYZ”⟩
17 1 2 3 4 5 6 7 8 5 6 11 9 7 10 13 16 14 15 12 tgfscgr φZ-˙A=Z-˙B