# 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}={\mathrm{Base}}_{{G}}$
colperpex.d
colperpex.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
colperpex.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
colperpex.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
colperpexlem.s ${⊢}{S}={pInv}_{𝒢}\left({G}\right)$
colperpexlem.m ${⊢}{M}={S}\left({A}\right)$
colperpexlem.n ${⊢}{N}={S}\left({B}\right)$
colperpexlem.k ${⊢}{K}={S}\left({Q}\right)$
colperpexlem.a ${⊢}{\phi }\to {A}\in {P}$
colperpexlem.b ${⊢}{\phi }\to {B}\in {P}$
colperpexlem.c ${⊢}{\phi }\to {C}\in {P}$
colperpexlem.q ${⊢}{\phi }\to {Q}\in {P}$
colperpexlem.1 ${⊢}{\phi }\to ⟨“{A}{B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
colperpexlem.2 ${⊢}{\phi }\to {K}\left({M}\left({C}\right)\right)={N}\left({C}\right)$
Assertion colperpexlem1 ${⊢}{\phi }\to ⟨“{B}{A}{Q}”⟩\in {∟}_{𝒢}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 colperpex.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 colperpex.d
3 colperpex.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 colperpex.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
5 colperpex.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
6 colperpexlem.s ${⊢}{S}={pInv}_{𝒢}\left({G}\right)$
7 colperpexlem.m ${⊢}{M}={S}\left({A}\right)$
8 colperpexlem.n ${⊢}{N}={S}\left({B}\right)$
9 colperpexlem.k ${⊢}{K}={S}\left({Q}\right)$
10 colperpexlem.a ${⊢}{\phi }\to {A}\in {P}$
11 colperpexlem.b ${⊢}{\phi }\to {B}\in {P}$
12 colperpexlem.c ${⊢}{\phi }\to {C}\in {P}$
13 colperpexlem.q ${⊢}{\phi }\to {Q}\in {P}$
14 colperpexlem.1 ${⊢}{\phi }\to ⟨“{A}{B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
15 colperpexlem.2 ${⊢}{\phi }\to {K}\left({M}\left({C}\right)\right)={N}\left({C}\right)$
16 1 2 3 4 6 5 10 7 13 mircl ${⊢}{\phi }\to {M}\left({Q}\right)\in {P}$
17 1 2 3 4 6 5 10 7 12 mircl ${⊢}{\phi }\to {M}\left({C}\right)\in {P}$
18 eqid ${⊢}{S}\left({B}\right)={S}\left({B}\right)$
19 1 2 3 4 6 5 11 18 12 mircl ${⊢}{\phi }\to {S}\left({B}\right)\left({C}\right)\in {P}$
20 1 2 3 4 6 5 10 7 19 mircl ${⊢}{\phi }\to {M}\left({S}\left({B}\right)\left({C}\right)\right)\in {P}$
21 1 2 3 4 6 5 11 8 12 mircl ${⊢}{\phi }\to {N}\left({C}\right)\in {P}$
22 15 21 eqeltrd ${⊢}{\phi }\to {K}\left({M}\left({C}\right)\right)\in {P}$
23 1 2 3 4 6 5 13 9 17 mirbtwn ${⊢}{\phi }\to {Q}\in \left({K}\left({M}\left({C}\right)\right){I}{M}\left({C}\right)\right)$
24 1 2 3 5 22 13 17 23 tgbtwncom ${⊢}{\phi }\to {Q}\in \left({M}\left({C}\right){I}{K}\left({M}\left({C}\right)\right)\right)$
25 8 fveq1i ${⊢}{N}\left({C}\right)={S}\left({B}\right)\left({C}\right)$
26 15 25 syl6eq ${⊢}{\phi }\to {K}\left({M}\left({C}\right)\right)={S}\left({B}\right)\left({C}\right)$
27 26 oveq2d ${⊢}{\phi }\to {M}\left({C}\right){I}{K}\left({M}\left({C}\right)\right)={M}\left({C}\right){I}{S}\left({B}\right)\left({C}\right)$
28 24 27 eleqtrd ${⊢}{\phi }\to {Q}\in \left({M}\left({C}\right){I}{S}\left({B}\right)\left({C}\right)\right)$
29 1 2 3 5 17 13 19 28 tgbtwncom ${⊢}{\phi }\to {Q}\in \left({S}\left({B}\right)\left({C}\right){I}{M}\left({C}\right)\right)$
30 1 2 3 4 6 5 10 7 19 13 17 29 mirbtwni ${⊢}{\phi }\to {M}\left({Q}\right)\in \left({M}\left({S}\left({B}\right)\left({C}\right)\right){I}{M}\left({M}\left({C}\right)\right)\right)$
31 1 2 3 4 6 5 10 7 12 mirmir ${⊢}{\phi }\to {M}\left({M}\left({C}\right)\right)={C}$
32 31 oveq2d ${⊢}{\phi }\to {M}\left({S}\left({B}\right)\left({C}\right)\right){I}{M}\left({M}\left({C}\right)\right)={M}\left({S}\left({B}\right)\left({C}\right)\right){I}{C}$
33 30 32 eleqtrd ${⊢}{\phi }\to {M}\left({Q}\right)\in \left({M}\left({S}\left({B}\right)\left({C}\right)\right){I}{C}\right)$
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 ${⊢}{\phi }\to {M}\left({M}\left({B}\right)\right)={B}$
45 eqidd ${⊢}{\phi }\to {M}\left({B}\right)={M}\left({B}\right)$
46 eqidd ${⊢}{\phi }\to {M}\left({C}\right)={M}\left({C}\right)$
47 44 45 46 s3eqd ${⊢}{\phi }\to ⟨“{M}\left({M}\left({B}\right)\right){M}\left({B}\right){M}\left({C}\right)”⟩=⟨“{B}{M}\left({B}\right){M}\left({C}\right)”⟩$
48 1 2 3 4 6 5 10 7 11 mircl ${⊢}{\phi }\to {M}\left({B}\right)\in {P}$
49 simpr ${⊢}\left({\phi }\wedge {A}={B}\right)\to {A}={B}$
50 49 fveq2d ${⊢}\left({\phi }\wedge {A}={B}\right)\to {M}\left({A}\right)={M}\left({B}\right)$
51 5 adantr ${⊢}\left({\phi }\wedge {A}={B}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
52 10 adantr ${⊢}\left({\phi }\wedge {A}={B}\right)\to {A}\in {P}$
53 1 2 3 4 6 51 52 7 mircinv ${⊢}\left({\phi }\wedge {A}={B}\right)\to {M}\left({A}\right)={A}$
54 50 53 eqtr3d ${⊢}\left({\phi }\wedge {A}={B}\right)\to {M}\left({B}\right)={A}$
55 eqidd ${⊢}\left({\phi }\wedge {A}={B}\right)\to {B}={B}$
56 eqidd ${⊢}\left({\phi }\wedge {A}={B}\right)\to {C}={C}$
57 54 55 56 s3eqd ${⊢}\left({\phi }\wedge {A}={B}\right)\to ⟨“{M}\left({B}\right){B}{C}”⟩=⟨“{A}{B}{C}”⟩$
58 14 adantr ${⊢}\left({\phi }\wedge {A}={B}\right)\to ⟨“{A}{B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
59 57 58 eqeltrd ${⊢}\left({\phi }\wedge {A}={B}\right)\to ⟨“{M}\left({B}\right){B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
60 5 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
61 10 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\in {P}$
62 11 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {B}\in {P}$
63 12 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {C}\in {P}$
64 1 2 3 4 6 60 61 7 62 mircl ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left({B}\right)\in {P}$
65 14 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to ⟨“{A}{B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
66 simpr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\ne {B}$
67 1 2 3 4 6 60 61 7 62 mirbtwn ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\in \left({M}\left({B}\right){I}{B}\right)$
68 1 4 3 60 64 62 61 67 btwncolg1 ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left({A}\in \left({M}\left({B}\right){L}{B}\right)\vee {M}\left({B}\right)={B}\right)$
69 1 4 3 60 64 62 61 68 colcom ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left({A}\in \left({B}{L}{M}\left({B}\right)\right)\vee {B}={M}\left({B}\right)\right)$
70 1 2 3 4 6 60 61 62 63 64 65 66 69 ragcol ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to ⟨“{M}\left({B}\right){B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
71 59 70 pm2.61dane ${⊢}{\phi }\to ⟨“{M}\left({B}\right){B}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
72 1 2 3 4 6 5 48 11 12 71 7 10 mirrag ${⊢}{\phi }\to ⟨“{M}\left({M}\left({B}\right)\right){M}\left({B}\right){M}\left({C}\right)”⟩\in {∟}_{𝒢}\left({G}\right)$
73 47 72 eqeltrrd ${⊢}{\phi }\to ⟨“{B}{M}\left({B}\right){M}\left({C}\right)”⟩\in {∟}_{𝒢}\left({G}\right)$
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 ${⊢}{\phi }\to {M}\left({S}\left({B}\right)\left({C}\right)\right)={S}\left({M}\left({B}\right)\right)\left({M}\left({C}\right)\right)$
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}\left({Q}\right)={S}\left({A}\right)\left({Q}\right)$
85 84 oveq2i
86 83 85 syl6eq
87 1 2 3 4 6 5 11 10 13 israg
88 86 87 mpbird ${⊢}{\phi }\to ⟨“{B}{A}{Q}”⟩\in {∟}_{𝒢}\left({G}\right)$