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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
colperpex.d ⊢ − = ( dist ‘ 𝐺 )
colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
colperpexlem.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
colperpexlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
colperpexlem.n ⊢ 𝑁 = ( 𝑆 ‘ 𝐵 )
colperpexlem.k ⊢ 𝐾 = ( 𝑆 ‘ 𝑄 )
colperpexlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
colperpexlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
colperpexlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
colperpexlem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
colperpexlem.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
colperpexlem.2 ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( 𝑁 ‘ 𝐶 ) )
Assertion colperpexlem1 ( 𝜑 → ⟨“ 𝐵 𝐴 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 colperpex.d ⊢ − = ( dist ‘ 𝐺 )
3 colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 colperpexlem.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
7 colperpexlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8 colperpexlem.n ⊢ 𝑁 = ( 𝑆 ‘ 𝐵 )
9 colperpexlem.k ⊢ 𝐾 = ( 𝑆 ‘ 𝑄 )
10 colperpexlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
11 colperpexlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
12 colperpexlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
13 colperpexlem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
14 colperpexlem.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
15 colperpexlem.2 ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( 𝑁 ‘ 𝐶 ) )
16 1 2 3 4 6 5 10 7 13 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑄 ) ∈ 𝑃 )
17 1 2 3 4 6 5 10 7 12 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐶 ) ∈ 𝑃 )
18 eqid ⊢ ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐵 )
19 1 2 3 4 6 5 11 18 12 mircl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ∈ 𝑃 )
20 1 2 3 4 6 5 10 7 19 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ∈ 𝑃 )
21 1 2 3 4 6 5 11 8 12 mircl ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐶 ) ∈ 𝑃 )
22 15 21 eqeltrd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) ∈ 𝑃 )
23 1 2 3 4 6 5 13 9 17 mirbtwn ⊢ ( 𝜑 → 𝑄 ∈ ( ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) 𝐼 ( 𝑀 ‘ 𝐶 ) ) )
24 1 2 3 5 22 13 17 23 tgbtwncom ⊢ ( 𝜑 → 𝑄 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) ) )
25 8 fveq1i ⊢ ( 𝑁 ‘ 𝐶 ) = ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 )
26 15 25 eqtrdi ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) )
27 26 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐶 ) 𝐼 ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) ) = ( ( 𝑀 ‘ 𝐶 ) 𝐼 ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
28 24 27 eleqtrd ⊢ ( 𝜑 → 𝑄 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
29 1 2 3 5 17 13 19 28 tgbtwncom ⊢ ( 𝜑 → 𝑄 ∈ ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) 𝐼 ( 𝑀 ‘ 𝐶 ) ) )
30 1 2 3 4 6 5 10 7 19 13 17 29 mirbtwni ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑄 ) ∈ ( ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) 𝐼 ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) ) )
31 1 2 3 4 6 5 10 7 12 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) = 𝐶 )
32 31 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) 𝐼 ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) ) = ( ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) 𝐼 𝐶 ) )
33 30 32 eleqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑄 ) ∈ ( ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) 𝐼 𝐶 ) )
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 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐵 ) ) = 𝐵 )
45 eqidd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ 𝐵 ) )
46 eqidd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐶 ) = ( 𝑀 ‘ 𝐶 ) )
47 44 45 46 s3eqd ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ ( 𝑀 ‘ 𝐵 ) ) ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ = ⟨“ 𝐵 ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ )
48 1 2 3 4 6 5 10 7 11 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
50 49 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐵 ) )
51 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
52 10 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
53 1 2 3 4 6 51 52 7 mircinv ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
54 50 53 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐵 ) = 𝐴 )
55 eqidd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 = 𝐵 )
56 eqidd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐶 = 𝐶 )
57 54 55 56 s3eqd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ⟨“ ( 𝑀 ‘ 𝐵 ) 𝐵 𝐶 ”⟩ = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
58 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
59 57 58 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ⟨“ ( 𝑀 ‘ 𝐵 ) 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
60 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
61 10 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
62 11 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
63 12 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ∈ 𝑃 )
64 1 2 3 4 6 60 61 7 62 mircl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
65 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
66 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
67 1 2 3 4 6 60 61 7 62 mirbtwn ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐼 𝐵 ) )
68 1 4 3 60 64 62 61 67 btwncolg1 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐿 𝐵 ) ∨ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) )
69 1 4 3 60 64 62 61 68 colcom ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) ∨ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) )
70 1 2 3 4 6 60 61 62 63 64 65 66 69 ragcol ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ⟨“ ( 𝑀 ‘ 𝐵 ) 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
71 59 70 pm2.61dane ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝐵 ) 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
72 1 2 3 4 6 5 48 11 12 71 7 10 mirrag ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ ( 𝑀 ‘ 𝐵 ) ) ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
73 47 72 eqeltrrd ⊢ ( 𝜑 → ⟨“ 𝐵 ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
74 1 2 3 4 6 5 11 48 17 israg ⊢ ( 𝜑 → ( ⟨“ 𝐵 ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐵 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐵 − ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) ) ) )
75 73 74 mpbid ⊢ ( 𝜑 → ( 𝐵 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐵 − ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) ) )
76 1 2 3 4 6 5 10 7 12 11 mirmir2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) )
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 ⊢ ( 𝑀 ‘ 𝑄 ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑄 )
85 84 oveq2i ⊢ ( 𝐵 − ( 𝑀 ‘ 𝑄 ) ) = ( 𝐵 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑄 ) )
86 83 85 eqtrdi ⊢ ( 𝜑 → ( 𝐵 − 𝑄 ) = ( 𝐵 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑄 ) ) )
87 1 2 3 4 6 5 11 10 13 israg ⊢ ( 𝜑 → ( ⟨“ 𝐵 𝐴 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐵 − 𝑄 ) = ( 𝐵 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑄 ) ) ) )
88 86 87 mpbird ⊢ ( 𝜑 → ⟨“ 𝐵 𝐴 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )