Proof of Theorem colperpexlem1
Step | Hyp | Ref
| Expression |
1 | | colperpex.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | colperpex.d |
. . . 4
⊢ − =
(dist‘𝐺) |
3 | | colperpex.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
4 | | colperpex.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | | colperpexlem.q |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝑃) |
6 | | colperpexlem.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
7 | | colperpex.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
8 | | colperpexlem.s |
. . . . 5
⊢ 𝑆 = (pInvG‘𝐺) |
9 | | colperpexlem.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
10 | | colperpexlem.m |
. . . . 5
⊢ 𝑀 = (𝑆‘𝐴) |
11 | 1, 2, 3, 7, 8, 4, 9, 10, 5 | mircl 27022 |
. . . 4
⊢ (𝜑 → (𝑀‘𝑄) ∈ 𝑃) |
12 | | colperpexlem.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
13 | 1, 2, 3, 7, 8, 4, 9, 10, 12 | mircl 27022 |
. . . . 5
⊢ (𝜑 → (𝑀‘𝐶) ∈ 𝑃) |
14 | | eqid 2738 |
. . . . . 6
⊢ (𝑆‘𝐵) = (𝑆‘𝐵) |
15 | 1, 2, 3, 7, 8, 4, 6, 14, 12 | mircl 27022 |
. . . . 5
⊢ (𝜑 → ((𝑆‘𝐵)‘𝐶) ∈ 𝑃) |
16 | 1, 2, 3, 7, 8, 4, 9, 10, 15 | mircl 27022 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑆‘𝐵)‘𝐶)) ∈ 𝑃) |
17 | | colperpexlem.2 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘(𝑀‘𝐶)) = (𝑁‘𝐶)) |
18 | | colperpexlem.n |
. . . . . . . . 9
⊢ 𝑁 = (𝑆‘𝐵) |
19 | 1, 2, 3, 7, 8, 4, 6, 18, 12 | mircl 27022 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘𝐶) ∈ 𝑃) |
20 | 17, 19 | eqeltrd 2839 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘(𝑀‘𝐶)) ∈ 𝑃) |
21 | | colperpexlem.k |
. . . . . . . 8
⊢ 𝐾 = (𝑆‘𝑄) |
22 | 1, 2, 3, 7, 8, 4, 5, 21, 13 | mirbtwn 27019 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ((𝐾‘(𝑀‘𝐶))𝐼(𝑀‘𝐶))) |
23 | 1, 2, 3, 4, 20, 5,
13, 22 | tgbtwncom 26849 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ((𝑀‘𝐶)𝐼(𝐾‘(𝑀‘𝐶)))) |
24 | 18 | fveq1i 6775 |
. . . . . . . 8
⊢ (𝑁‘𝐶) = ((𝑆‘𝐵)‘𝐶) |
25 | 17, 24 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘(𝑀‘𝐶)) = ((𝑆‘𝐵)‘𝐶)) |
26 | 25 | oveq2d 7291 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝐶)𝐼(𝐾‘(𝑀‘𝐶))) = ((𝑀‘𝐶)𝐼((𝑆‘𝐵)‘𝐶))) |
27 | 23, 26 | eleqtrd 2841 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ ((𝑀‘𝐶)𝐼((𝑆‘𝐵)‘𝐶))) |
28 | 1, 2, 3, 4, 13, 5,
15, 27 | tgbtwncom 26849 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ (((𝑆‘𝐵)‘𝐶)𝐼(𝑀‘𝐶))) |
29 | 1, 2, 3, 7, 8, 4, 9, 10, 15, 5, 13, 28 | mirbtwni 27032 |
. . . . . 6
⊢ (𝜑 → (𝑀‘𝑄) ∈ ((𝑀‘((𝑆‘𝐵)‘𝐶))𝐼(𝑀‘(𝑀‘𝐶)))) |
30 | 1, 2, 3, 7, 8, 4, 9, 10, 12 | mirmir 27023 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘(𝑀‘𝐶)) = 𝐶) |
31 | 30 | oveq2d 7291 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘((𝑆‘𝐵)‘𝐶))𝐼(𝑀‘(𝑀‘𝐶))) = ((𝑀‘((𝑆‘𝐵)‘𝐶))𝐼𝐶)) |
32 | 29, 31 | eleqtrd 2841 |
. . . . 5
⊢ (𝜑 → (𝑀‘𝑄) ∈ ((𝑀‘((𝑆‘𝐵)‘𝐶))𝐼𝐶)) |
33 | 1, 2, 3, 4, 13, 15 | axtgcgrrflx 26823 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝐶) − ((𝑆‘𝐵)‘𝐶)) = (((𝑆‘𝐵)‘𝐶) − (𝑀‘𝐶))) |
34 | 1, 2, 3, 7, 8, 4, 9, 10, 15, 13 | miriso 27031 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘((𝑆‘𝐵)‘𝐶)) − (𝑀‘(𝑀‘𝐶))) = (((𝑆‘𝐵)‘𝐶) − (𝑀‘𝐶))) |
35 | 30 | oveq2d 7291 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘((𝑆‘𝐵)‘𝐶)) − (𝑀‘(𝑀‘𝐶))) = ((𝑀‘((𝑆‘𝐵)‘𝐶)) − 𝐶)) |
36 | 33, 34, 35 | 3eqtr2d 2784 |
. . . . 5
⊢ (𝜑 → ((𝑀‘𝐶) − ((𝑆‘𝐵)‘𝐶)) = ((𝑀‘((𝑆‘𝐵)‘𝐶)) − 𝐶)) |
37 | 25 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 → (𝑄 − (𝐾‘(𝑀‘𝐶))) = (𝑄 − ((𝑆‘𝐵)‘𝐶))) |
38 | 1, 2, 3, 7, 8, 4, 5, 21, 13 | mircgr 27018 |
. . . . . . 7
⊢ (𝜑 → (𝑄 − (𝐾‘(𝑀‘𝐶))) = (𝑄 − (𝑀‘𝐶))) |
39 | 37, 38 | eqtr3d 2780 |
. . . . . 6
⊢ (𝜑 → (𝑄 − ((𝑆‘𝐵)‘𝐶)) = (𝑄 − (𝑀‘𝐶))) |
40 | 1, 2, 3, 7, 8, 4, 9, 10, 5, 13 | miriso 27031 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝑄) − (𝑀‘(𝑀‘𝐶))) = (𝑄 − (𝑀‘𝐶))) |
41 | 30 | oveq2d 7291 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝑄) − (𝑀‘(𝑀‘𝐶))) = ((𝑀‘𝑄) − 𝐶)) |
42 | 39, 40, 41 | 3eqtr2d 2784 |
. . . . 5
⊢ (𝜑 → (𝑄 − ((𝑆‘𝐵)‘𝐶)) = ((𝑀‘𝑄) − 𝐶)) |
43 | 1, 2, 3, 7, 8, 4, 9, 10, 6 | mirmir 27023 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀‘(𝑀‘𝐵)) = 𝐵) |
44 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐵) = (𝑀‘𝐵)) |
45 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐶) = (𝑀‘𝐶)) |
46 | 43, 44, 45 | s3eqd 14577 |
. . . . . . . . 9
⊢ (𝜑 → 〈“(𝑀‘(𝑀‘𝐵))(𝑀‘𝐵)(𝑀‘𝐶)”〉 = 〈“𝐵(𝑀‘𝐵)(𝑀‘𝐶)”〉) |
47 | 1, 2, 3, 7, 8, 4, 9, 10, 6 | mircl 27022 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝑃) |
48 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
49 | 48 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑀‘𝐴) = (𝑀‘𝐵)) |
50 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ TarskiG) |
51 | 9 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝑃) |
52 | 1, 2, 3, 7, 8, 50,
51, 10 | mircinv 27029 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑀‘𝐴) = 𝐴) |
53 | 49, 52 | eqtr3d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑀‘𝐵) = 𝐴) |
54 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 = 𝐵) |
55 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐶) |
56 | 53, 54, 55 | s3eqd 14577 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 〈“(𝑀‘𝐵)𝐵𝐶”〉 = 〈“𝐴𝐵𝐶”〉) |
57 | | colperpexlem.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
58 | 57 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
59 | 56, 58 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 〈“(𝑀‘𝐵)𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
60 | 4 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
61 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
62 | 6 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
63 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐶 ∈ 𝑃) |
64 | 1, 2, 3, 7, 8, 60,
61, 10, 62 | mircl 27022 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑀‘𝐵) ∈ 𝑃) |
65 | 57 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
66 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
67 | 1, 2, 3, 7, 8, 60,
61, 10, 62 | mirbtwn 27019 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)) |
68 | 1, 7, 3, 60, 64, 62, 61, 67 | btwncolg1 26916 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 ∈ ((𝑀‘𝐵)𝐿𝐵) ∨ (𝑀‘𝐵) = 𝐵)) |
69 | 1, 7, 3, 60, 64, 62, 61, 68 | colcom 26919 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 ∈ (𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵))) |
70 | 1, 2, 3, 7, 8, 60,
61, 62, 63, 64, 65, 66, 69 | ragcol 27060 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 〈“(𝑀‘𝐵)𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
71 | 59, 70 | pm2.61dane 3032 |
. . . . . . . . . 10
⊢ (𝜑 → 〈“(𝑀‘𝐵)𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
72 | 1, 2, 3, 7, 8, 4, 47, 6, 12, 71, 10, 9 | mirrag 27062 |
. . . . . . . . 9
⊢ (𝜑 → 〈“(𝑀‘(𝑀‘𝐵))(𝑀‘𝐵)(𝑀‘𝐶)”〉 ∈ (∟G‘𝐺)) |
73 | 46, 72 | eqeltrrd 2840 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐵(𝑀‘𝐵)(𝑀‘𝐶)”〉 ∈ (∟G‘𝐺)) |
74 | 1, 2, 3, 7, 8, 4, 6, 47, 13 | israg 27058 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐵(𝑀‘𝐵)(𝑀‘𝐶)”〉 ∈ (∟G‘𝐺) ↔ (𝐵 − (𝑀‘𝐶)) = (𝐵 − ((𝑆‘(𝑀‘𝐵))‘(𝑀‘𝐶))))) |
75 | 73, 74 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − (𝑀‘𝐶)) = (𝐵 − ((𝑆‘(𝑀‘𝐵))‘(𝑀‘𝐶)))) |
76 | 1, 2, 3, 7, 8, 4, 9, 10, 12, 6 | mirmir2 27035 |
. . . . . . . 8
⊢ (𝜑 → (𝑀‘((𝑆‘𝐵)‘𝐶)) = ((𝑆‘(𝑀‘𝐵))‘(𝑀‘𝐶))) |
77 | 76 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − (𝑀‘((𝑆‘𝐵)‘𝐶))) = (𝐵 − ((𝑆‘(𝑀‘𝐵))‘(𝑀‘𝐶)))) |
78 | 75, 77 | eqtr4d 2781 |
. . . . . 6
⊢ (𝜑 → (𝐵 − (𝑀‘𝐶)) = (𝐵 − (𝑀‘((𝑆‘𝐵)‘𝐶)))) |
79 | 1, 2, 3, 4, 6, 13,
6, 16, 78 | tgcgrcomlr 26841 |
. . . . 5
⊢ (𝜑 → ((𝑀‘𝐶) − 𝐵) = ((𝑀‘((𝑆‘𝐵)‘𝐶)) − 𝐵)) |
80 | 1, 2, 3, 7, 8, 4, 6, 14, 12 | mircgr 27018 |
. . . . . 6
⊢ (𝜑 → (𝐵 − ((𝑆‘𝐵)‘𝐶)) = (𝐵 − 𝐶)) |
81 | 1, 2, 3, 4, 6, 15,
6, 12, 80 | tgcgrcomlr 26841 |
. . . . 5
⊢ (𝜑 → (((𝑆‘𝐵)‘𝐶) − 𝐵) = (𝐶 − 𝐵)) |
82 | 1, 2, 3, 4, 13, 5,
15, 6, 16, 11, 12, 6, 27, 32, 36, 42, 79, 81 | tgifscgr 26869 |
. . . 4
⊢ (𝜑 → (𝑄 − 𝐵) = ((𝑀‘𝑄) − 𝐵)) |
83 | 1, 2, 3, 4, 5, 6, 11, 6, 82 | tgcgrcomlr 26841 |
. . 3
⊢ (𝜑 → (𝐵 − 𝑄) = (𝐵 − (𝑀‘𝑄))) |
84 | 10 | fveq1i 6775 |
. . . 4
⊢ (𝑀‘𝑄) = ((𝑆‘𝐴)‘𝑄) |
85 | 84 | oveq2i 7286 |
. . 3
⊢ (𝐵 − (𝑀‘𝑄)) = (𝐵 − ((𝑆‘𝐴)‘𝑄)) |
86 | 83, 85 | eqtrdi 2794 |
. 2
⊢ (𝜑 → (𝐵 − 𝑄) = (𝐵 − ((𝑆‘𝐴)‘𝑄))) |
87 | 1, 2, 3, 7, 8, 4, 6, 9, 5 | israg 27058 |
. 2
⊢ (𝜑 → (〈“𝐵𝐴𝑄”〉 ∈ (∟G‘𝐺) ↔ (𝐵 − 𝑄) = (𝐵 − ((𝑆‘𝐴)‘𝑄)))) |
88 | 86, 87 | mpbird 256 |
1
⊢ (𝜑 → 〈“𝐵𝐴𝑄”〉 ∈ (∟G‘𝐺)) |