# Metamath Proof Explorer

## Theorem colperpexlem1

Description: Lemma for colperp . First part of lemma 8.20 of Schwabhauser p. 62. (Contributed by Thierry Arnoux, 27-Oct-2019)

Ref Expression
Hypotheses colperpex.p $⊢ P = Base G$
colperpex.d
colperpex.i $⊢ I = Itv ⁡ G$
colperpex.l $⊢ L = Line 𝒢 ⁡ G$
colperpex.g $⊢ φ → G ∈ 𝒢 Tarski$
colperpexlem.s $⊢ S = pInv 𝒢 ⁡ G$
colperpexlem.m $⊢ M = S ⁡ A$
colperpexlem.n $⊢ N = S ⁡ B$
colperpexlem.k $⊢ K = S ⁡ Q$
colperpexlem.a $⊢ φ → A ∈ P$
colperpexlem.b $⊢ φ → B ∈ P$
colperpexlem.c $⊢ φ → C ∈ P$
colperpexlem.q $⊢ φ → Q ∈ P$
colperpexlem.1 $⊢ φ → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G$
colperpexlem.2 $⊢ φ → K ⁡ M ⁡ C = N ⁡ C$
Assertion colperpexlem1 $⊢ φ → ⟨“ BAQ ”⟩ ∈ ∟ 𝒢 ⁡ G$

### Proof

Step Hyp Ref Expression
1 colperpex.p $⊢ P = Base G$
2 colperpex.d
3 colperpex.i $⊢ I = Itv ⁡ G$
4 colperpex.l $⊢ L = Line 𝒢 ⁡ G$
5 colperpex.g $⊢ φ → G ∈ 𝒢 Tarski$
6 colperpexlem.s $⊢ S = pInv 𝒢 ⁡ G$
7 colperpexlem.m $⊢ M = S ⁡ A$
8 colperpexlem.n $⊢ N = S ⁡ B$
9 colperpexlem.k $⊢ K = S ⁡ Q$
10 colperpexlem.a $⊢ φ → A ∈ P$
11 colperpexlem.b $⊢ φ → B ∈ P$
12 colperpexlem.c $⊢ φ → C ∈ P$
13 colperpexlem.q $⊢ φ → Q ∈ P$
14 colperpexlem.1 $⊢ φ → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G$
15 colperpexlem.2 $⊢ φ → K ⁡ M ⁡ C = N ⁡ C$
16 1 2 3 4 6 5 10 7 13 mircl $⊢ φ → M ⁡ Q ∈ P$
17 1 2 3 4 6 5 10 7 12 mircl $⊢ φ → M ⁡ C ∈ P$
18 eqid $⊢ S ⁡ B = S ⁡ B$
19 1 2 3 4 6 5 11 18 12 mircl $⊢ φ → S ⁡ B ⁡ C ∈ P$
20 1 2 3 4 6 5 10 7 19 mircl $⊢ φ → M ⁡ S ⁡ B ⁡ C ∈ P$
21 1 2 3 4 6 5 11 8 12 mircl $⊢ φ → N ⁡ C ∈ P$
22 15 21 eqeltrd $⊢ φ → K ⁡ M ⁡ C ∈ P$
23 1 2 3 4 6 5 13 9 17 mirbtwn $⊢ φ → Q ∈ K ⁡ M ⁡ C I M ⁡ C$
24 1 2 3 5 22 13 17 23 tgbtwncom $⊢ φ → Q ∈ M ⁡ C I K ⁡ M ⁡ C$
25 8 fveq1i $⊢ N ⁡ C = S ⁡ B ⁡ C$
26 15 25 eqtrdi $⊢ φ → K ⁡ M ⁡ C = S ⁡ B ⁡ C$
27 26 oveq2d $⊢ φ → M ⁡ C I K ⁡ M ⁡ C = M ⁡ C I S ⁡ B ⁡ C$
28 24 27 eleqtrd $⊢ φ → Q ∈ M ⁡ C I S ⁡ B ⁡ C$
29 1 2 3 5 17 13 19 28 tgbtwncom $⊢ φ → Q ∈ S ⁡ B ⁡ C I M ⁡ C$
30 1 2 3 4 6 5 10 7 19 13 17 29 mirbtwni $⊢ φ → M ⁡ Q ∈ M ⁡ S ⁡ B ⁡ C I M ⁡ M ⁡ C$
31 1 2 3 4 6 5 10 7 12 mirmir $⊢ φ → M ⁡ M ⁡ C = C$
32 31 oveq2d $⊢ φ → M ⁡ S ⁡ B ⁡ C I M ⁡ M ⁡ C = M ⁡ S ⁡ B ⁡ C I C$
33 30 32 eleqtrd $⊢ φ → M ⁡ Q ∈ M ⁡ S ⁡ B ⁡ C I C$
34 1 2 3 5 17 19 axtgcgrrflx
35 1 2 3 4 6 5 10 7 19 17 miriso
36 31 oveq2d
37 34 35 36 3eqtr2d
38 26 oveq2d
39 1 2 3 4 6 5 13 9 17 mircgr
40 38 39 eqtr3d
41 1 2 3 4 6 5 10 7 13 17 miriso
42 31 oveq2d
43 40 41 42 3eqtr2d
44 1 2 3 4 6 5 10 7 11 mirmir $⊢ φ → M ⁡ M ⁡ B = B$
45 eqidd $⊢ φ → M ⁡ B = M ⁡ B$
46 eqidd $⊢ φ → M ⁡ C = M ⁡ C$
47 44 45 46 s3eqd $⊢ φ → ⟨“ M ⁡ M ⁡ B M ⁡ B M ⁡ C ”⟩ = ⟨“ B M ⁡ B M ⁡ C ”⟩$
48 1 2 3 4 6 5 10 7 11 mircl $⊢ φ → M ⁡ B ∈ P$
49 simpr $⊢ φ ∧ A = B → A = B$
50 49 fveq2d $⊢ φ ∧ A = B → M ⁡ A = M ⁡ B$
51 5 adantr $⊢ φ ∧ A = B → G ∈ 𝒢 Tarski$
52 10 adantr $⊢ φ ∧ A = B → A ∈ P$
53 1 2 3 4 6 51 52 7 mircinv $⊢ φ ∧ A = B → M ⁡ A = A$
54 50 53 eqtr3d $⊢ φ ∧ A = B → M ⁡ B = A$
55 eqidd $⊢ φ ∧ A = B → B = B$
56 eqidd $⊢ φ ∧ A = B → C = C$
57 54 55 56 s3eqd $⊢ φ ∧ A = B → ⟨“ M ⁡ B BC ”⟩ = ⟨“ ABC ”⟩$
58 14 adantr $⊢ φ ∧ A = B → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G$
59 57 58 eqeltrd $⊢ φ ∧ A = B → ⟨“ M ⁡ B BC ”⟩ ∈ ∟ 𝒢 ⁡ G$
60 5 adantr $⊢ φ ∧ A ≠ B → G ∈ 𝒢 Tarski$
61 10 adantr $⊢ φ ∧ A ≠ B → A ∈ P$
62 11 adantr $⊢ φ ∧ A ≠ B → B ∈ P$
63 12 adantr $⊢ φ ∧ A ≠ B → C ∈ P$
64 1 2 3 4 6 60 61 7 62 mircl $⊢ φ ∧ A ≠ B → M ⁡ B ∈ P$
65 14 adantr $⊢ φ ∧ A ≠ B → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G$
66 simpr $⊢ φ ∧ A ≠ B → A ≠ B$
67 1 2 3 4 6 60 61 7 62 mirbtwn $⊢ φ ∧ A ≠ B → A ∈ M ⁡ B I B$
68 1 4 3 60 64 62 61 67 btwncolg1 $⊢ φ ∧ A ≠ B → A ∈ M ⁡ B L B ∨ M ⁡ B = B$
69 1 4 3 60 64 62 61 68 colcom $⊢ φ ∧ A ≠ B → A ∈ B L M ⁡ B ∨ B = M ⁡ B$
70 1 2 3 4 6 60 61 62 63 64 65 66 69 ragcol $⊢ φ ∧ A ≠ B → ⟨“ M ⁡ B BC ”⟩ ∈ ∟ 𝒢 ⁡ G$
71 59 70 pm2.61dane $⊢ φ → ⟨“ M ⁡ B BC ”⟩ ∈ ∟ 𝒢 ⁡ G$
72 1 2 3 4 6 5 48 11 12 71 7 10 mirrag $⊢ φ → ⟨“ M ⁡ M ⁡ B M ⁡ B M ⁡ C ”⟩ ∈ ∟ 𝒢 ⁡ G$
73 47 72 eqeltrrd $⊢ φ → ⟨“ B M ⁡ B M ⁡ C ”⟩ ∈ ∟ 𝒢 ⁡ G$
74 1 2 3 4 6 5 11 48 17 israg
75 73 74 mpbid
76 1 2 3 4 6 5 10 7 12 11 mirmir2 $⊢ φ → M ⁡ S ⁡ B ⁡ C = S ⁡ M ⁡ B ⁡ M ⁡ C$
77 76 oveq2d
78 75 77 eqtr4d
79 1 2 3 5 11 17 11 20 78 tgcgrcomlr
80 1 2 3 4 6 5 11 18 12 mircgr
81 1 2 3 5 11 19 11 12 80 tgcgrcomlr
82 1 2 3 5 17 13 19 11 20 16 12 11 28 33 37 43 79 81 tgifscgr
83 1 2 3 5 13 11 16 11 82 tgcgrcomlr
84 7 fveq1i $⊢ M ⁡ Q = S ⁡ A ⁡ Q$
85 84 oveq2i
86 83 85 eqtrdi
87 1 2 3 4 6 5 11 10 13 israg
88 86 87 mpbird $⊢ φ → ⟨“ BAQ ”⟩ ∈ ∟ 𝒢 ⁡ G$