Metamath Proof Explorer


Theorem tgcgrsub2

Description: Removing identical parts from the end of a line segment preserves congruence. In this version the order of points is not known. (Contributed by Thierry Arnoux, 3-Apr-2019)

Ref Expression
Hypotheses legval.p 𝑃 = ( Base ‘ 𝐺 )
legval.d = ( dist ‘ 𝐺 )
legval.i 𝐼 = ( Itv ‘ 𝐺 )
legval.l = ( ≤G ‘ 𝐺 )
legval.g ( 𝜑𝐺 ∈ TarskiG )
legid.a ( 𝜑𝐴𝑃 )
legid.b ( 𝜑𝐵𝑃 )
legtrd.c ( 𝜑𝐶𝑃 )
legtrd.d ( 𝜑𝐷𝑃 )
tgcgrsub2.d ( 𝜑𝐷𝑃 )
tgcgrsub2.e ( 𝜑𝐸𝑃 )
tgcgrsub2.f ( 𝜑𝐹𝑃 )
tgcgrsub2.1 ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
tgcgrsub2.2 ( 𝜑 → ( 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ) )
tgcgrsub2.3 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
tgcgrsub2.4 ( 𝜑 → ( 𝐴 𝐶 ) = ( 𝐷 𝐹 ) )
Assertion tgcgrsub2 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )

Proof

Step Hyp Ref Expression
1 legval.p 𝑃 = ( Base ‘ 𝐺 )
2 legval.d = ( dist ‘ 𝐺 )
3 legval.i 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l = ( ≤G ‘ 𝐺 )
5 legval.g ( 𝜑𝐺 ∈ TarskiG )
6 legid.a ( 𝜑𝐴𝑃 )
7 legid.b ( 𝜑𝐵𝑃 )
8 legtrd.c ( 𝜑𝐶𝑃 )
9 legtrd.d ( 𝜑𝐷𝑃 )
10 tgcgrsub2.d ( 𝜑𝐷𝑃 )
11 tgcgrsub2.e ( 𝜑𝐸𝑃 )
12 tgcgrsub2.f ( 𝜑𝐹𝑃 )
13 tgcgrsub2.1 ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
14 tgcgrsub2.2 ( 𝜑 → ( 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ) )
15 tgcgrsub2.3 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
16 tgcgrsub2.4 ( 𝜑 → ( 𝐴 𝐶 ) = ( 𝐷 𝐹 ) )
17 5 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
18 8 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶𝑃 )
19 7 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵𝑃 )
20 12 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐹𝑃 )
21 11 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐸𝑃 )
22 6 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴𝑃 )
23 9 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐷𝑃 )
24 simpr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
25 1 2 3 17 22 19 18 24 tgbtwncom ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
26 14 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ) )
27 1 2 3 4 17 22 19 18 24 btwnleg ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐴 𝐵 ) ( 𝐴 𝐶 ) )
28 15 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
29 16 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐴 𝐶 ) = ( 𝐷 𝐹 ) )
30 27 28 29 3brtr3d ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐷 𝐸 ) ( 𝐷 𝐹 ) )
31 1 2 3 4 17 21 20 23 23 26 30 legbtwn ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
32 1 2 3 17 23 21 20 31 tgbtwncom ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐸 ∈ ( 𝐹 𝐼 𝐷 ) )
33 1 2 3 5 6 8 9 12 16 tgcgrcomlr ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
34 33 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
35 1 2 3 5 6 7 9 11 15 tgcgrcomlr ( 𝜑 → ( 𝐵 𝐴 ) = ( 𝐸 𝐷 ) )
36 35 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐵 𝐴 ) = ( 𝐸 𝐷 ) )
37 1 2 3 17 18 19 22 20 21 23 25 32 34 36 tgcgrsub ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐶 𝐵 ) = ( 𝐹 𝐸 ) )
38 1 2 3 17 18 19 20 21 37 tgcgrcomlr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
39 5 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
40 7 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵𝑃 )
41 8 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶𝑃 )
42 6 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴𝑃 )
43 11 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐸𝑃 )
44 12 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐹𝑃 )
45 9 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐷𝑃 )
46 simpr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
47 1 2 3 39 42 41 40 46 tgbtwncom ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) )
48 14 orcomd ( 𝜑 → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
49 48 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
50 1 2 3 4 39 42 41 40 46 btwnleg ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝐶 ) ( 𝐴 𝐵 ) )
51 16 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝐶 ) = ( 𝐷 𝐹 ) )
52 15 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
53 50 51 52 3brtr3d ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐷 𝐹 ) ( 𝐷 𝐸 ) )
54 1 2 3 4 39 44 43 45 45 49 53 legbtwn ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) )
55 1 2 3 39 45 44 43 54 tgbtwncom ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) )
56 35 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐵 𝐴 ) = ( 𝐸 𝐷 ) )
57 33 adantr ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
58 1 2 3 39 40 41 42 43 44 45 47 55 56 57 tgcgrsub ( ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
59 38 58 13 mpjaodan ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )