Metamath Proof Explorer

Theorem tgaaddcpbllem2

Description: Lemma for tgaaddcpbl . (Contributed by Thierry Arnoux, 2-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl.p ⊢ P = Base G
tgaaddcpbl.i ⊢ I = Itv ⁡ G
tgaaddcpbl.l ⊢ L = Line 𝒢 ⁡ G
tgaaddcpbl.c ⊢ ∼ ˙ = ∼ 𝒢 ∠ ⁡ G
tgaaddcpbl.o ⊢ O = a b | a ∈ P ∖ Y L S ∧ b ∈ P ∖ Y L S ∧ ∃ s ∈ Y L S s ∈ a I b
tgaaddcpbl.q ⊢ Q = c d | c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ∧ ∃ t ∈ V L T t ∈ c I d
tgaaddcpbl.1 ⊢ φ → G ∈ 𝒢 Tarski
tgaaddcpbl.s ⊢ φ → S ∈ P
tgaaddcpbl.t ⊢ φ → T ∈ P
tgaaddcpbl.u ⊢ φ → U ∈ P
tgaaddcpbl.v ⊢ φ → V ∈ P
tgaaddcpbl.w ⊢ φ → W ∈ P
tgaaddcpbl.x ⊢ φ → X ∈ P
tgaaddcpbl.y ⊢ φ → Y ∈ P
tgaaddcpbl.z ⊢ φ → Z ∈ P
tgaaddcpbl.2 ⊢ φ → Y ≠ S
tgaaddcpbl.3 ⊢ φ → V ≠ T
tgaaddcpbl.4 ⊢ φ → X O Z
tgaaddcpbl.5 ⊢ φ → U Q W
tgaaddcpbl.6 ⊢ φ → ⟨“ XYS ”⟩ ∼ ˙ ⟨“ UVT ”⟩
tgaaddcpbl.7 ⊢ φ → ⟨“ SYZ ”⟩ ∼ ˙ ⟨“ TVW ”⟩
tgaaddcpbllem3.1 ⊢ φ → ¬ Y ∈ X I Z
tgaaddcpbllem2.1 ⊢ φ → R ∈ Y L S
tgaaddcpbllem2.2 ⊢ φ → R ∈ X I Z
tgaaddcpbllem2.3 ⊢ φ → Y ∈ S I R
tgaaddcpbllem2.m ⊢ M = pInv 𝒢 ⁡ G ⁡ V
tgaaddcpbllem2.k ⊢ K = hl 𝒢 ⁡ G
Assertion tgaaddcpbllem2 ⊢ φ → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩

Proof

Step Hyp Ref Expression
1 tgaaddcpbl.p ⊢ P = Base G
2 tgaaddcpbl.i ⊢ I = Itv ⁡ G
3 tgaaddcpbl.l ⊢ L = Line 𝒢 ⁡ G
4 tgaaddcpbl.c ⊢ ∼ ˙ = ∼ 𝒢 ∠ ⁡ G
5 tgaaddcpbl.o ⊢ O = a b | a ∈ P ∖ Y L S ∧ b ∈ P ∖ Y L S ∧ ∃ s ∈ Y L S s ∈ a I b
6 tgaaddcpbl.q ⊢ Q = c d | c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ∧ ∃ t ∈ V L T t ∈ c I d
7 tgaaddcpbl.1 ⊢ φ → G ∈ 𝒢 Tarski
8 tgaaddcpbl.s ⊢ φ → S ∈ P
9 tgaaddcpbl.t ⊢ φ → T ∈ P
10 tgaaddcpbl.u ⊢ φ → U ∈ P
11 tgaaddcpbl.v ⊢ φ → V ∈ P
12 tgaaddcpbl.w ⊢ φ → W ∈ P
13 tgaaddcpbl.x ⊢ φ → X ∈ P
14 tgaaddcpbl.y ⊢ φ → Y ∈ P
15 tgaaddcpbl.z ⊢ φ → Z ∈ P
16 tgaaddcpbl.2 ⊢ φ → Y ≠ S
17 tgaaddcpbl.3 ⊢ φ → V ≠ T
18 tgaaddcpbl.4 ⊢ φ → X O Z
19 tgaaddcpbl.5 ⊢ φ → U Q W
20 tgaaddcpbl.6 ⊢ φ → ⟨“ XYS ”⟩ ∼ ˙ ⟨“ UVT ”⟩
21 tgaaddcpbl.7 ⊢ φ → ⟨“ SYZ ”⟩ ∼ ˙ ⟨“ TVW ”⟩
22 tgaaddcpbllem3.1 ⊢ φ → ¬ Y ∈ X I Z
23 tgaaddcpbllem2.1 ⊢ φ → R ∈ Y L S
24 tgaaddcpbllem2.2 ⊢ φ → R ∈ X I Z
25 tgaaddcpbllem2.3 ⊢ φ → Y ∈ S I R
26 tgaaddcpbllem2.m ⊢ M = pInv 𝒢 ⁡ G ⁡ V
27 tgaaddcpbllem2.k ⊢ K = hl 𝒢 ⁡ G
28 eleq1w ⊢ e = s → e ∈ a I b ↔ s ∈ a I b
29 28 cbvrexvw ⊢ ∃ e ∈ Y L R e ∈ a I b ↔ ∃ s ∈ Y L R s ∈ a I b
30 29 anbi2i ⊢ a ∈ P ∖ Y L R ∧ b ∈ P ∖ Y L R ∧ ∃ e ∈ Y L R e ∈ a I b ↔ a ∈ P ∖ Y L R ∧ b ∈ P ∖ Y L R ∧ ∃ s ∈ Y L R s ∈ a I b
31 30 opabbii ⊢ a b | a ∈ P ∖ Y L R ∧ b ∈ P ∖ Y L R ∧ ∃ e ∈ Y L R e ∈ a I b = a b | a ∈ P ∖ Y L R ∧ b ∈ P ∖ Y L R ∧ ∃ s ∈ Y L R s ∈ a I b
32 eleq1w ⊢ a = c → a ∈ P ∖ V L M ⁡ T ↔ c ∈ P ∖ V L M ⁡ T
33 eleq1w ⊢ b = d → b ∈ P ∖ V L M ⁡ T ↔ d ∈ P ∖ V L M ⁡ T
34 32 33 bi2anan9 ⊢ a = c ∧ b = d → a ∈ P ∖ V L M ⁡ T ∧ b ∈ P ∖ V L M ⁡ T ↔ c ∈ P ∖ V L M ⁡ T ∧ d ∈ P ∖ V L M ⁡ T
35 oveq12 ⊢ a = c ∧ b = d → a I b = c I d
36 35 eleq2d ⊢ a = c ∧ b = d → f ∈ a I b ↔ f ∈ c I d
37 36 rexbidv ⊢ a = c ∧ b = d → ∃ f ∈ V L M ⁡ T f ∈ a I b ↔ ∃ f ∈ V L M ⁡ T f ∈ c I d
38 eleq1w ⊢ f = t → f ∈ c I d ↔ t ∈ c I d
39 38 cbvrexvw ⊢ ∃ f ∈ V L M ⁡ T f ∈ c I d ↔ ∃ t ∈ V L M ⁡ T t ∈ c I d
40 37 39 bitrdi ⊢ a = c ∧ b = d → ∃ f ∈ V L M ⁡ T f ∈ a I b ↔ ∃ t ∈ V L M ⁡ T t ∈ c I d
41 34 40 anbi12d ⊢ a = c ∧ b = d → a ∈ P ∖ V L M ⁡ T ∧ b ∈ P ∖ V L M ⁡ T ∧ ∃ f ∈ V L M ⁡ T f ∈ a I b ↔ c ∈ P ∖ V L M ⁡ T ∧ d ∈ P ∖ V L M ⁡ T ∧ ∃ t ∈ V L M ⁡ T t ∈ c I d
42 41 cbvopabv ⊢ a b | a ∈ P ∖ V L M ⁡ T ∧ b ∈ P ∖ V L M ⁡ T ∧ ∃ f ∈ V L M ⁡ T f ∈ a I b = c d | c ∈ P ∖ V L M ⁡ T ∧ d ∈ P ∖ V L M ⁡ T ∧ ∃ t ∈ V L M ⁡ T t ∈ c I d
43 1 2 3 7 14 8 16 tgelrnln ⊢ φ → Y L S ∈ ran ⁡ L
44 1 3 2 7 43 23 tglnpt ⊢ φ → R ∈ P
45 eqid ⊢ dist ⁡ G = dist ⁡ G
46 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
47 1 45 2 3 46 7 11 26 9 mircl ⊢ φ → M ⁡ T ∈ P
48 24 22 elnelneq2d ⊢ φ → ¬ R = Y
49 48 neqned ⊢ φ → R ≠ Y
50 49 necomd ⊢ φ → Y ≠ R
51 17 necomd ⊢ φ → T ≠ V
52 1 45 2 3 46 7 11 26 9 51 mirne ⊢ φ → M ⁡ T ≠ V
53 52 necomd ⊢ φ → V ≠ M ⁡ T
54 1 2 3 7 14 44 50 tglinerflx2 ⊢ φ → R ∈ Y L R
55 1 45 2 5 3 43 7 13 15 18 oppne1 ⊢ φ → ¬ X ∈ Y L S
56 1 2 3 7 14 8 16 44 49 23 tglineelsb2 ⊢ φ → Y L S = Y L R
57 55 56 neleqtrd ⊢ φ → ¬ X ∈ Y L R
58 1 45 2 5 3 43 7 13 15 18 oppne2 ⊢ φ → ¬ Z ∈ Y L S
59 58 56 neleqtrd ⊢ φ → ¬ Z ∈ Y L R
60 1 45 2 31 13 15 54 57 59 24 islnoppd ⊢ φ → X a b | a ∈ P ∖ Y L R ∧ b ∈ P ∖ Y L R ∧ ∃ e ∈ Y L R e ∈ a I b Z
61 1 45 2 3 46 7 11 26 9 mirbtwn ⊢ φ → V ∈ M ⁡ T I T
62 1 2 3 7 11 9 47 17 61 btwnlng2 ⊢ φ → M ⁡ T ∈ V L T
63 1 2 3 7 11 9 17 47 52 62 tglineelsb2 ⊢ φ → V L T = V L M ⁡ T
64 63 difeq2d ⊢ φ → P ∖ V L T = P ∖ V L M ⁡ T
65 64 eleq2d ⊢ φ → c ∈ P ∖ V L T ↔ c ∈ P ∖ V L M ⁡ T
66 64 eleq2d ⊢ φ → d ∈ P ∖ V L T ↔ d ∈ P ∖ V L M ⁡ T
67 65 66 anbi12d ⊢ φ → c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ↔ c ∈ P ∖ V L M ⁡ T ∧ d ∈ P ∖ V L M ⁡ T
68 63 rexeqdv ⊢ φ → ∃ t ∈ V L T t ∈ c I d ↔ ∃ t ∈ V L M ⁡ T t ∈ c I d
69 67 68 anbi12d ⊢ φ → c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ∧ ∃ t ∈ V L T t ∈ c I d ↔ c ∈ P ∖ V L M ⁡ T ∧ d ∈ P ∖ V L M ⁡ T ∧ ∃ t ∈ V L M ⁡ T t ∈ c I d
70 69 opabbidv ⊢ φ → c d | c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ∧ ∃ t ∈ V L T t ∈ c I d = c d | c ∈ P ∖ V L M ⁡ T ∧ d ∈ P ∖ V L M ⁡ T ∧ ∃ t ∈ V L M ⁡ T t ∈ c I d
71 70 6 42 3eqtr4g ⊢ φ → Q = a b | a ∈ P ∖ V L M ⁡ T ∧ b ∈ P ∖ V L M ⁡ T ∧ ∃ f ∈ V L M ⁡ T f ∈ a I b
72 71 19 breqdi ⊢ φ → U a b | a ∈ P ∖ V L M ⁡ T ∧ b ∈ P ∖ V L M ⁡ T ∧ ∃ f ∈ V L M ⁡ T f ∈ a I b W
73 4 a1i ⊢ φ → ∼ ˙ = ∼ 𝒢 ∠ ⁡ G
74 73 eqcomd ⊢ φ → ∼ 𝒢 ∠ ⁡ G = ∼ ˙
75 73 20 breqdi ⊢ φ → ⟨“ XYS ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UVT ”⟩
76 1 2 45 7 13 14 8 10 11 9 75 cgraswaplr ⊢ φ → ⟨“ SYX ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ TVU ”⟩
77 1 45 2 7 47 11 9 61 tgbtwncom ⊢ φ → V ∈ T I M ⁡ T
78 1 2 45 7 8 14 13 9 11 10 44 47 76 25 77 50 53 sacgr ⊢ φ → ⟨“ RYX ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ M ⁡ T VU ”⟩
79 1 2 45 7 44 14 13 47 11 10 78 cgraswaplr ⊢ φ → ⟨“ XYR ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UV M ⁡ T ”⟩
80 74 79 breqdi ⊢ φ → ⟨“ XYR ”⟩ ∼ ˙ ⟨“ UV M ⁡ T ”⟩
81 73 21 breqdi ⊢ φ → ⟨“ SYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ TVW ”⟩
82 1 2 45 7 8 14 15 9 11 12 44 47 81 25 77 50 53 sacgr ⊢ φ → ⟨“ RYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ M ⁡ T VW ”⟩
83 74 82 breqdi ⊢ φ → ⟨“ RYZ ”⟩ ∼ ˙ ⟨“ M ⁡ T VW ”⟩
84 1 2 27 44 13 14 7 49 hlid ⊢ φ → R K ⁡ Y R
85 1 2 3 4 31 42 7 44 47 10 11 12 13 14 15 50 53 60 72 80 83 22 27 54 24 84 tgaaddcpbllem1 ⊢ φ → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩