Metamath Proof Explorer


Theorem lnxfr

Description: Transfer law for colinearity. Theorem 4.13 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tglngval.p P = Base G
tglngval.l L = Line 𝒢 G
tglngval.i I = Itv G
tglngval.g φ G 𝒢 Tarski
tglngval.x φ X P
tglngval.y φ Y P
tgcolg.z φ Z P
lnxfr.r ˙ = 𝒢 G
lnxfr.a φ A P
lnxfr.b φ B P
lnxfr.c φ C P
lnxfr.1 φ Y X L Z X = Z
lnxfr.2 φ ⟨“ XYZ ”⟩ ˙ ⟨“ ABC ”⟩
Assertion lnxfr φ B A L C A = C

Proof

Step Hyp Ref Expression
1 tglngval.p P = Base G
2 tglngval.l L = Line 𝒢 G
3 tglngval.i I = Itv G
4 tglngval.g φ G 𝒢 Tarski
5 tglngval.x φ X P
6 tglngval.y φ Y P
7 tgcolg.z φ Z P
8 lnxfr.r ˙ = 𝒢 G
9 lnxfr.a φ A P
10 lnxfr.b φ B P
11 lnxfr.c φ C P
12 lnxfr.1 φ Y X L Z X = Z
13 lnxfr.2 φ ⟨“ XYZ ”⟩ ˙ ⟨“ ABC ”⟩
14 4 adantr φ Y X I Z G 𝒢 Tarski
15 9 adantr φ Y X I Z A P
16 11 adantr φ Y X I Z C P
17 10 adantr φ Y X I Z B P
18 eqid dist G = dist G
19 5 adantr φ Y X I Z X P
20 6 adantr φ Y X I Z Y P
21 7 adantr φ Y X I Z Z P
22 13 adantr φ Y X I Z ⟨“ XYZ ”⟩ ˙ ⟨“ ABC ”⟩
23 simpr φ Y X I Z Y X I Z
24 1 18 3 8 14 19 20 21 15 17 16 22 23 tgbtwnxfr φ Y X I Z B A I C
25 1 2 3 14 15 16 17 24 btwncolg1 φ Y X I Z B A L C A = C
26 4 adantr φ X Y I Z G 𝒢 Tarski
27 9 adantr φ X Y I Z A P
28 11 adantr φ X Y I Z C P
29 10 adantr φ X Y I Z B P
30 6 adantr φ X Y I Z Y P
31 5 adantr φ X Y I Z X P
32 7 adantr φ X Y I Z Z P
33 13 adantr φ X Y I Z ⟨“ XYZ ”⟩ ˙ ⟨“ ABC ”⟩
34 1 18 3 8 26 31 30 32 27 29 28 33 cgr3swap12 φ X Y I Z ⟨“ YXZ ”⟩ ˙ ⟨“ BAC ”⟩
35 simpr φ X Y I Z X Y I Z
36 1 18 3 8 26 30 31 32 29 27 28 34 35 tgbtwnxfr φ X Y I Z A B I C
37 1 2 3 26 27 28 29 36 btwncolg2 φ X Y I Z B A L C A = C
38 4 adantr φ Z X I Y G 𝒢 Tarski
39 9 adantr φ Z X I Y A P
40 11 adantr φ Z X I Y C P
41 10 adantr φ Z X I Y B P
42 5 adantr φ Z X I Y X P
43 7 adantr φ Z X I Y Z P
44 6 adantr φ Z X I Y Y P
45 13 adantr φ Z X I Y ⟨“ XYZ ”⟩ ˙ ⟨“ ABC ”⟩
46 1 18 3 8 38 42 44 43 39 41 40 45 cgr3swap23 φ Z X I Y ⟨“ XZY ”⟩ ˙ ⟨“ ACB ”⟩
47 simpr φ Z X I Y Z X I Y
48 1 18 3 8 38 42 43 44 39 40 41 46 47 tgbtwnxfr φ Z X I Y C A I B
49 1 2 3 38 39 40 41 48 btwncolg3 φ Z X I Y B A L C A = C
50 1 2 3 4 5 7 6 tgcolg φ Y X L Z X = Z Y X I Z X Y I Z Z X I Y
51 12 50 mpbid φ Y X I Z X Y I Z Z X I Y
52 25 37 49 51 mpjao3dan φ B A L C A = C