Metamath Proof Explorer

Theorem cgraswap

Description: Swap rays in a congruence relation. Theorem 11.9 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020)

Ref Expression
Hypotheses cgraid.p ⊢ P = Base G
cgraid.i ⊢ I = Itv ⁡ G
cgraid.g ⊢ φ → G ∈ 𝒢 Tarski
cgraid.k ⊢ K = hl 𝒢 ⁡ G
cgraid.a ⊢ φ → A ∈ P
cgraid.b ⊢ φ → B ∈ P
cgraid.c ⊢ φ → C ∈ P
cgraid.1 ⊢ φ → A ≠ B
cgraid.2 ⊢ φ → B ≠ C
Assertion cgraswap ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ CBA ”⟩

Proof

Step Hyp Ref Expression
1 cgraid.p ⊢ P = Base G
2 cgraid.i ⊢ I = Itv ⁡ G
3 cgraid.g ⊢ φ → G ∈ 𝒢 Tarski
4 cgraid.k ⊢ K = hl 𝒢 ⁡ G
5 cgraid.a ⊢ φ → A ∈ P
6 cgraid.b ⊢ φ → B ∈ P
7 cgraid.c ⊢ φ → C ∈ P
8 cgraid.1 ⊢ φ → A ≠ B
9 cgraid.2 ⊢ φ → B ≠ C
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 eqid ⊢ ∼ 𝒢 ⁡ G = ∼ 𝒢 ⁡ G
12 3 ad3antrrr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → G ∈ 𝒢 Tarski
13 5 ad3antrrr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → A ∈ P
14 6 ad3antrrr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → B ∈ P
15 7 ad3antrrr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → C ∈ P
16 simpllr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x ∈ P
17 simplr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → y ∈ P
18 simprlr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → B dist ⁡ G x = B dist ⁡ G A
19 1 10 2 12 14 16 14 13 18 tgcgrcomlr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x dist ⁡ G B = A dist ⁡ G B
20 19 eqcomd ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → A dist ⁡ G B = x dist ⁡ G B
21 simprrr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → B dist ⁡ G y = B dist ⁡ G C
22 21 eqcomd ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → B dist ⁡ G C = B dist ⁡ G y
23 eqid ⊢ Line 𝒢 ⁡ G = Line 𝒢 ⁡ G
24 simprll ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x K ⁡ B C
25 1 2 4 16 15 14 12 23 24 hlln ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x ∈ C Line 𝒢 ⁡ G B
26 25 orcd ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x ∈ C Line 𝒢 ⁡ G B ∨ C = B
27 1 23 2 12 15 14 16 26 colrot1 ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → C ∈ B Line 𝒢 ⁡ G x ∨ B = x
28 eqid ⊢ ≤ 𝒢 ⁡ G = ≤ 𝒢 ⁡ G
29 1 2 4 16 15 14 12 ishlg ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x K ⁡ B C ↔ x ≠ B ∧ C ≠ B ∧ x ∈ B I C ∨ C ∈ B I x
30 24 29 mpbid ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x ≠ B ∧ C ≠ B ∧ x ∈ B I C ∨ C ∈ B I x
31 30 simp3d ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x ∈ B I C ∨ C ∈ B I x
32 31 orcomd ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → C ∈ B I x ∨ x ∈ B I C
33 simprrl ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → y K ⁡ B A
34 1 2 4 17 13 14 12 ishlg ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → y K ⁡ B A ↔ y ≠ B ∧ A ≠ B ∧ y ∈ B I A ∨ A ∈ B I y
35 33 34 mpbid ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → y ≠ B ∧ A ≠ B ∧ y ∈ B I A ∨ A ∈ B I y
36 35 simp3d ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → y ∈ B I A ∨ A ∈ B I y
37 1 10 2 28 12 14 15 16 14 14 17 13 32 36 22 18 tgcgrsub2 ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → C dist ⁡ G x = y dist ⁡ G A
38 1 10 11 12 14 15 16 14 17 13 22 37 19 trgcgr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → ⟨“ BCx ”⟩ ∼ 𝒢 ⁡ G ⟨“ ByA ”⟩
39 1 10 2 12 15 17 axtgcgrrflx ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → C dist ⁡ G y = y dist ⁡ G C
40 9 ad3antrrr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → B ≠ C
41 1 23 2 12 14 15 16 11 14 17 10 17 13 15 27 38 21 39 40 tgfscgr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → x dist ⁡ G y = A dist ⁡ G C
42 1 10 2 12 16 17 13 15 41 tgcgrcomlr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → y dist ⁡ G x = C dist ⁡ G A
43 42 eqcomd ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → C dist ⁡ G A = y dist ⁡ G x
44 1 10 11 12 13 14 15 16 14 17 20 22 43 trgcgr ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ xBy ”⟩
45 44 24 33 3jca ⊢ φ ∧ x ∈ P ∧ y ∈ P ∧ x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C → ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ xBy ”⟩ ∧ x K ⁡ B C ∧ y K ⁡ B A
46 9 necomd ⊢ φ → C ≠ B
47 8 necomd ⊢ φ → B ≠ A
48 1 2 4 6 6 5 3 7 10 46 47 hlcgrex ⊢ φ → ∃ x ∈ P x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A
49 1 2 4 6 6 7 3 5 10 8 9 hlcgrex ⊢ φ → ∃ y ∈ P y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C
50 reeanv ⊢ ∃ x ∈ P ∃ y ∈ P x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C ↔ ∃ x ∈ P x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ ∃ y ∈ P y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C
51 48 49 50 sylanbrc ⊢ φ → ∃ x ∈ P ∃ y ∈ P x K ⁡ B C ∧ B dist ⁡ G x = B dist ⁡ G A ∧ y K ⁡ B A ∧ B dist ⁡ G y = B dist ⁡ G C
52 45 51 reximddv2 ⊢ φ → ∃ x ∈ P ∃ y ∈ P ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ xBy ”⟩ ∧ x K ⁡ B C ∧ y K ⁡ B A
53 1 2 4 3 5 6 7 7 6 5 iscgra ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ CBA ”⟩ ↔ ∃ x ∈ P ∃ y ∈ P ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ xBy ”⟩ ∧ x K ⁡ B C ∧ y K ⁡ B A
54 52 53 mpbird ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ CBA ”⟩