Proof of Theorem ragcgr
| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 = 𝐷) |
| 2 | | israg.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
| 3 | | israg.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
| 4 | | israg.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
| 5 | | israg.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐺 ∈ TarskiG) |
| 7 | | israg.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ 𝑃) |
| 9 | | israg.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐶 ∈ 𝑃) |
| 11 | | ragcgr.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 ∈ 𝑃) |
| 13 | | ragcgr.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐹 ∈ 𝑃) |
| 15 | | ragcgr.c |
. . . . . 6
⊢ ∼ =
(cgrG‘𝐺) |
| 16 | | israg.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐴 ∈ 𝑃) |
| 18 | | ragcgr.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 19 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 ∈ 𝑃) |
| 20 | | ragcgr.2 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) |
| 21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) |
| 22 | 2, 3, 4, 15, 6, 17, 8, 10, 19, 12, 14, 21 | cgr3simp2 28529 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 23 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶) |
| 24 | 2, 3, 4, 6, 8, 10,
12, 14, 22, 23 | tgcgreq 28490 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 = 𝐹) |
| 25 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐹 = 𝐹) |
| 26 | 1, 24, 25 | s3eqd 14903 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 〈“𝐷𝐸𝐹”〉 = 〈“𝐷𝐹𝐹”〉) |
| 27 | | israg.l |
. . . 4
⊢ 𝐿 = (LineG‘𝐺) |
| 28 | | israg.s |
. . . 4
⊢ 𝑆 = (pInvG‘𝐺) |
| 29 | 2, 3, 4, 27, 28, 6, 19, 14, 12 | ragtrivb 28710 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 〈“𝐷𝐹𝐹”〉 ∈ (∟G‘𝐺)) |
| 30 | 26, 29 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
| 31 | | ragcgr.1 |
. . . . . 6
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
| 32 | 31 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
| 33 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐺 ∈ TarskiG) |
| 34 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐴 ∈ 𝑃) |
| 35 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ 𝑃) |
| 36 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐶 ∈ 𝑃) |
| 37 | 2, 3, 4, 27, 28, 33, 34, 35, 36 | israg 28705 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)))) |
| 38 | 32, 37 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶))) |
| 39 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐹 ∈ 𝑃) |
| 40 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐷 ∈ 𝑃) |
| 41 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ 𝑃) |
| 42 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) |
| 43 | 2, 3, 4, 15, 33, 34, 35, 36, 40, 41, 39, 42 | cgr3simp3 28530 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 44 | 2, 3, 4, 33, 36, 34, 39, 40, 43 | tgcgrcomlr 28488 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 45 | | eqid 2737 |
. . . . . 6
⊢ (𝑆‘𝐵) = (𝑆‘𝐵) |
| 46 | 2, 3, 4, 27, 28, 33, 35, 45, 36 | mircl 28669 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ((𝑆‘𝐵)‘𝐶) ∈ 𝑃) |
| 47 | | eqid 2737 |
. . . . . 6
⊢ (𝑆‘𝐸) = (𝑆‘𝐸) |
| 48 | 2, 3, 4, 27, 28, 33, 41, 47, 39 | mircl 28669 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ((𝑆‘𝐸)‘𝐹) ∈ 𝑃) |
| 49 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐶) |
| 50 | 49 | necomd 2996 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐶 ≠ 𝐵) |
| 51 | 2, 3, 4, 27, 28, 33, 35, 45, 36 | mirbtwn 28666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ (((𝑆‘𝐵)‘𝐶)𝐼𝐶)) |
| 52 | 2, 3, 4, 33, 46, 35, 36, 51 | tgbtwncom 28496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ (𝐶𝐼((𝑆‘𝐵)‘𝐶))) |
| 53 | 2, 3, 4, 27, 28, 33, 41, 47, 39 | mirbtwn 28666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ (((𝑆‘𝐸)‘𝐹)𝐼𝐹)) |
| 54 | 2, 3, 4, 33, 48, 41, 39, 53 | tgbtwncom 28496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ (𝐹𝐼((𝑆‘𝐸)‘𝐹))) |
| 55 | 2, 3, 4, 15, 33, 34, 35, 36, 40, 41, 39, 42 | cgr3simp2 28529 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 56 | 2, 3, 4, 33, 35, 36, 41, 39, 55 | tgcgrcomlr 28488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐶 − 𝐵) = (𝐹 − 𝐸)) |
| 57 | 2, 3, 4, 27, 28, 33, 35, 45, 36 | mircgr 28665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − ((𝑆‘𝐵)‘𝐶)) = (𝐵 − 𝐶)) |
| 58 | 2, 3, 4, 27, 28, 33, 41, 47, 39 | mircgr 28665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐸 − ((𝑆‘𝐸)‘𝐹)) = (𝐸 − 𝐹)) |
| 59 | 55, 57, 58 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − ((𝑆‘𝐵)‘𝐶)) = (𝐸 − ((𝑆‘𝐸)‘𝐹))) |
| 60 | 2, 3, 4, 15, 33, 34, 35, 36, 40, 41, 39, 42 | cgr3simp1 28528 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 61 | 2, 3, 4, 33, 34, 35, 40, 41, 60 | tgcgrcomlr 28488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
| 62 | 2, 3, 4, 33, 36, 35, 46, 39, 41, 48, 34, 40, 50, 52, 54, 56, 59, 43, 61 | axtg5seg 28473 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (((𝑆‘𝐵)‘𝐶) − 𝐴) = (((𝑆‘𝐸)‘𝐹) − 𝐷)) |
| 63 | 2, 3, 4, 33, 46, 34, 48, 40, 62 | tgcgrcomlr 28488 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − ((𝑆‘𝐵)‘𝐶)) = (𝐷 − ((𝑆‘𝐸)‘𝐹))) |
| 64 | 38, 44, 63 | 3eqtr3d 2785 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐷 − 𝐹) = (𝐷 − ((𝑆‘𝐸)‘𝐹))) |
| 65 | 2, 3, 4, 27, 28, 33, 40, 41, 39 | israg 28705 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺) ↔ (𝐷 − 𝐹) = (𝐷 − ((𝑆‘𝐸)‘𝐹)))) |
| 66 | 64, 65 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
| 67 | 30, 66 | pm2.61dane 3029 |
1
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |