Proof of Theorem lmiisolem
| Step | Hyp | Ref
| Expression |
| 1 | | ismid.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | ismid.d |
. . . . . . . 8
⊢ − =
(dist‘𝐺) |
| 3 | | ismid.i |
. . . . . . . 8
⊢ 𝐼 = (Itv‘𝐺) |
| 4 | | ismid.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐺 ∈ TarskiG) |
| 6 | | lmiisolem.z |
. . . . . . . . . 10
⊢ 𝑍 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 7 | | ismid.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
| 8 | | lmiiso.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 9 | | lmif.m |
. . . . . . . . . . . . 13
⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) |
| 10 | | lmif.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (LineG‘𝐺) |
| 11 | | lmif.d |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
| 12 | 1, 2, 3, 4, 7, 9, 10, 11, 8 | lmicl 28794 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑃) |
| 13 | 1, 2, 3, 4, 7, 8, 12 | midcl 28785 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃) |
| 14 | | lmiiso.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 15 | 1, 2, 3, 4, 7, 9, 10, 11, 14 | lmicl 28794 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝑃) |
| 16 | 1, 2, 3, 4, 7, 14,
15 | midcl 28785 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃) |
| 17 | 1, 2, 3, 4, 7, 13,
16 | midcl 28785 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ 𝑃) |
| 18 | 6, 17 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝑃) |
| 20 | | eqid 2737 |
. . . . . . . . . 10
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
| 21 | | lmiisolem.s |
. . . . . . . . . 10
⊢ 𝑆 = ((pInvG‘𝐺)‘𝑍) |
| 22 | 1, 2, 3, 10, 20, 4, 18, 21, 8 | mircl 28669 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐴) ∈ 𝑃) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) ∈ 𝑃) |
| 24 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝑃) |
| 25 | 1, 2, 3, 10, 20, 5, 19, 21, 24 | mircgr 28665 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴)) |
| 26 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) = 𝑍) |
| 27 | 26 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = (𝑆‘𝐴)) |
| 28 | 1, 2, 3, 5, 19, 23, 19, 24, 25, 27 | tgcgreq 28490 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = 𝐴) |
| 29 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 31 | 6, 30 | eqtr4id 2796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴)))) |
| 32 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐺 ∈ TarskiG) |
| 33 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐺DimTarskiG≥2) |
| 34 | 13 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃) |
| 35 | 1, 2, 3, 32, 33, 34, 34 | midid 28789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (𝐴(midG‘𝐺)(𝑀‘𝐴))) |
| 36 | 31, 35 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 = (𝐴(midG‘𝐺)(𝑀‘𝐴))) |
| 37 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀‘𝐴) = (𝑀‘𝐴)) |
| 38 | 1, 2, 3, 4, 7, 9, 10, 11, 8, 12 | islmib 28795 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀‘𝐴) = (𝑀‘𝐴) ↔ ((𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴))))) |
| 39 | 37, 38 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴)))) |
| 40 | 39 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷) |
| 41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷) |
| 42 | 36, 41 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝐷) |
| 43 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐺 ∈ TarskiG) |
| 44 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃) |
| 45 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃) |
| 46 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝑃) |
| 47 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 48 | 1, 2, 3, 4, 7, 13,
16 | midbtwn 28787 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 49 | 6, 48 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 51 | 1, 3, 10, 43, 44, 45, 46, 47, 50 | btwnlng1 28627 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 52 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 ∈ ran 𝐿) |
| 53 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷) |
| 54 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘𝐵) = (𝑀‘𝐵)) |
| 55 | 1, 2, 3, 4, 7, 9, 10, 11, 14, 15 | islmib 28795 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀‘𝐵) = (𝑀‘𝐵) ↔ ((𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵))))) |
| 56 | 54, 55 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵)))) |
| 57 | 56 | simpld 494 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷) |
| 59 | 1, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58 | tglinethru 28644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 60 | 51, 59 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝐷) |
| 61 | 42, 60 | pm2.61dane 3029 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ 𝐷) |
| 62 | 61 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝐷) |
| 63 | 28, 62 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝐷) |
| 64 | 1, 2, 3, 4, 7, 9, 10, 11, 8 | lmiinv 28800 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷)) |
| 65 | 64 | biimpar 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐷) → (𝑀‘𝐴) = 𝐴) |
| 66 | 63, 65 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝐴) |
| 67 | 66, 28 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝑍) |
| 68 | 67 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝑍 − (𝑀‘𝐵))) |
| 69 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝑍 = 𝑍) |
| 70 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐺 ∈ TarskiG) |
| 71 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 ∈ 𝑃) |
| 72 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃) |
| 73 | 1, 2, 3, 4, 7, 14,
15 | midbtwn 28787 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵))) |
| 74 | 73 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵))) |
| 75 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝑀‘𝐵)) |
| 76 | 75 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵𝐼𝐵) = (𝐵𝐼(𝑀‘𝐵))) |
| 77 | 74, 76 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼𝐵)) |
| 78 | 1, 2, 3, 70, 71, 72, 77 | axtgbtwnid 28474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 79 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = 𝐵) |
| 80 | 69, 78, 79 | s3eqd 14903 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 〈“𝑍𝐵𝐵”〉 = 〈“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”〉) |
| 81 | 1, 2, 3, 10, 20, 4, 18, 14, 14 | ragtrivb 28710 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝑍𝐵𝐵”〉 ∈ (∟G‘𝐺)) |
| 82 | 81 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 〈“𝑍𝐵𝐵”〉 ∈ (∟G‘𝐺)) |
| 83 | 80, 82 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 〈“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”〉 ∈ (∟G‘𝐺)) |
| 84 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐺 ∈ TarskiG) |
| 85 | 61 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝑍 ∈ 𝐷) |
| 86 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷) |
| 87 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐵 ∈ 𝑃) |
| 88 | | df-ne 2941 |
. . . . . . . . . 10
⊢ (𝐵 ≠ (𝑀‘𝐵) ↔ ¬ 𝐵 = (𝑀‘𝐵)) |
| 89 | 56 | simprd 495 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵))) |
| 90 | 89 | orcomd 872 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 = (𝑀‘𝐵) ∨ 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)))) |
| 91 | 90 | orcanai 1005 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐵 = (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵))) |
| 92 | 88, 91 | sylan2b 594 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵))) |
| 93 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝑀‘𝐵) ∈ 𝑃) |
| 94 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐵 ≠ (𝑀‘𝐵)) |
| 95 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃) |
| 96 | 4 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐺 ∈ TarskiG) |
| 97 | 14 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐵 ∈ 𝑃) |
| 98 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝑀‘𝐵) ∈ 𝑃) |
| 99 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐺DimTarskiG≥2) |
| 100 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) |
| 101 | 1, 2, 3, 96, 99, 97, 98, 100 | midcgr 28788 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − 𝐵) = (𝐵 − (𝑀‘𝐵))) |
| 102 | 101 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − (𝑀‘𝐵)) = (𝐵 − 𝐵)) |
| 103 | 1, 2, 3, 96, 97, 98, 97, 102 | axtgcgrid 28471 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐵 = (𝑀‘𝐵)) |
| 104 | 103 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵 → 𝐵 = (𝑀‘𝐵))) |
| 105 | 104 | necon3d 2961 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ≠ (𝑀‘𝐵) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ≠ 𝐵)) |
| 106 | 105 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ≠ 𝐵) |
| 107 | 73 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵))) |
| 108 | 1, 3, 10, 84, 87, 93, 95, 94, 107 | btwnlng1 28627 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐿(𝑀‘𝐵))) |
| 109 | 1, 3, 10, 84, 87, 93, 94, 95, 106, 108 | tglineelsb2 28640 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 110 | 1, 3, 10, 84, 95, 87, 106 | tglinecom 28643 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 111 | 109, 110 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵)) |
| 112 | 92, 111 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵)) |
| 113 | 1, 2, 3, 10, 84, 85, 86, 87, 112 | perpdrag 28736 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 〈“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”〉 ∈ (∟G‘𝐺)) |
| 114 | 83, 113 | pm2.61dane 3029 |
. . . . . 6
⊢ (𝜑 → 〈“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”〉 ∈ (∟G‘𝐺)) |
| 115 | 1, 2, 3, 10, 20, 4, 18, 16, 14 | israg 28705 |
. . . . . 6
⊢ (𝜑 → (〈“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”〉 ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))) |
| 116 | 114, 115 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))) |
| 117 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 118 | 1, 2, 3, 4, 7, 14,
15, 20, 16 | ismidb 28786 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) ↔ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 119 | 117, 118 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)) |
| 120 | 119 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝑍 − (𝑀‘𝐵)) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))) |
| 121 | 116, 120 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵))) |
| 122 | 121 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵))) |
| 123 | 28 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝐴 − 𝐵)) |
| 124 | 68, 122, 123 | 3eqtr2d 2783 |
. 2
⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |
| 125 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝐺 ∈ TarskiG) |
| 126 | 22 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑆‘𝐴) ∈ 𝑃) |
| 127 | 18 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ 𝑃) |
| 128 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝐴 ∈ 𝑃) |
| 129 | 1, 2, 3, 10, 20, 4, 18, 21, 12 | mircl 28669 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) ∈ 𝑃) |
| 130 | 129 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑆‘(𝑀‘𝐴)) ∈ 𝑃) |
| 131 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑀‘𝐴) ∈ 𝑃) |
| 132 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝐵 ∈ 𝑃) |
| 133 | 15 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑀‘𝐵) ∈ 𝑃) |
| 134 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑆‘𝐴) ≠ 𝑍) |
| 135 | 1, 2, 3, 10, 20, 125, 127, 21, 128 | mirbtwn 28666 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘𝐴)𝐼𝐴)) |
| 136 | 1, 2, 3, 10, 20, 125, 127, 21, 131 | mirbtwn 28666 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘(𝑀‘𝐴))𝐼(𝑀‘𝐴))) |
| 137 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝑍 = 𝑍) |
| 138 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐺 ∈ TarskiG) |
| 139 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 ∈ 𝑃) |
| 140 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃) |
| 141 | 1, 2, 3, 4, 7, 8, 12 | midbtwn 28787 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴))) |
| 142 | 141 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴))) |
| 143 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝑀‘𝐴)) |
| 144 | 143 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴𝐼𝐴) = (𝐴𝐼(𝑀‘𝐴))) |
| 145 | 142, 144 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼𝐴)) |
| 146 | 1, 2, 3, 138, 139, 140, 145 | axtgbtwnid 28474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝐴(midG‘𝐺)(𝑀‘𝐴))) |
| 147 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = 𝐴) |
| 148 | 137, 146,
147 | s3eqd 14903 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 〈“𝑍𝐴𝐴”〉 = 〈“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”〉) |
| 149 | 1, 2, 3, 10, 20, 4, 18, 8, 8 | ragtrivb 28710 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈“𝑍𝐴𝐴”〉 ∈ (∟G‘𝐺)) |
| 150 | 149 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 〈“𝑍𝐴𝐴”〉 ∈ (∟G‘𝐺)) |
| 151 | 148, 150 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 〈“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”〉 ∈ (∟G‘𝐺)) |
| 152 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐺 ∈ TarskiG) |
| 153 | 61 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝑍 ∈ 𝐷) |
| 154 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷) |
| 155 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐴 ∈ 𝑃) |
| 156 | | df-ne 2941 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ (𝑀‘𝐴) ↔ ¬ 𝐴 = (𝑀‘𝐴)) |
| 157 | 39 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴))) |
| 158 | 157 | orcomd 872 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 = (𝑀‘𝐴) ∨ 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)))) |
| 159 | 158 | orcanai 1005 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐴 = (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴))) |
| 160 | 156, 159 | sylan2b 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴))) |
| 161 | 12 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝑀‘𝐴) ∈ 𝑃) |
| 162 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐴 ≠ (𝑀‘𝐴)) |
| 163 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃) |
| 164 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐺 ∈ TarskiG) |
| 165 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐴 ∈ 𝑃) |
| 166 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝑀‘𝐴) ∈ 𝑃) |
| 167 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐺DimTarskiG≥2) |
| 168 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) |
| 169 | 1, 2, 3, 164, 167, 165, 166, 168 | midcgr 28788 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − 𝐴) = (𝐴 − (𝑀‘𝐴))) |
| 170 | 169 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − (𝑀‘𝐴)) = (𝐴 − 𝐴)) |
| 171 | 1, 2, 3, 164, 165, 166, 165, 170 | axtgcgrid 28471 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐴 = (𝑀‘𝐴)) |
| 172 | 171 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴 → 𝐴 = (𝑀‘𝐴))) |
| 173 | 172 | necon3d 2961 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ≠ (𝑀‘𝐴) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ 𝐴)) |
| 174 | 173 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ 𝐴) |
| 175 | 141 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴))) |
| 176 | 1, 3, 10, 152, 155, 161, 163, 162, 175 | btwnlng1 28627 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐿(𝑀‘𝐴))) |
| 177 | 1, 3, 10, 152, 155, 161, 162, 163, 174, 176 | tglineelsb2 28640 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴)))) |
| 178 | 1, 3, 10, 152, 163, 155, 174 | tglinecom 28643 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴)))) |
| 179 | 177, 178 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴)) |
| 180 | 160, 179 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴)) |
| 181 | 1, 2, 3, 10, 152, 153, 154, 155, 180 | perpdrag 28736 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 〈“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”〉 ∈ (∟G‘𝐺)) |
| 182 | 151, 181 | pm2.61dane 3029 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”〉 ∈ (∟G‘𝐺)) |
| 183 | 1, 2, 3, 10, 20, 4, 18, 13, 8 | israg 28705 |
. . . . . . . . 9
⊢ (𝜑 → (〈“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”〉 ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))) |
| 184 | 182, 183 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))) |
| 185 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴))) |
| 186 | 1, 2, 3, 4, 7, 8, 12, 20, 13 | ismidb 28786 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴) ↔ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))) |
| 187 | 185, 186 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)) |
| 188 | 187 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 − (𝑀‘𝐴)) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))) |
| 189 | 184, 188 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴))) |
| 190 | 1, 2, 3, 10, 20, 4, 18, 21, 8 | mircgr 28665 |
. . . . . . 7
⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴)) |
| 191 | 1, 2, 3, 10, 20, 4, 18, 21, 12 | mircgr 28665 |
. . . . . . 7
⊢ (𝜑 → (𝑍 − (𝑆‘(𝑀‘𝐴))) = (𝑍 − (𝑀‘𝐴))) |
| 192 | 189, 190,
191 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴)))) |
| 193 | 192 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴)))) |
| 194 | 1, 2, 3, 125, 127, 126, 127, 130, 193 | tgcgrcomlr 28488 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑆‘𝐴) − 𝑍) = ((𝑆‘(𝑀‘𝐴)) − 𝑍)) |
| 195 | 189 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴))) |
| 196 | 21 | fveq1i 6907 |
. . . . . . . . . 10
⊢ (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) |
| 197 | 1, 2, 3, 4, 7, 8, 12, 21, 18 | mirmid 28791 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))) |
| 198 | 6 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍 |
| 199 | 1, 2, 3, 4, 7, 13,
16, 20, 18 | ismidb 28786 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) ↔ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍)) |
| 200 | 198, 199 | mpbiri 258 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))) |
| 201 | 196, 197,
200 | 3eqtr4a 2803 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 202 | 1, 2, 3, 4, 7, 22,
129, 20, 16 | ismidb 28786 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)) ↔ ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))) |
| 203 | 201, 202 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))) |
| 204 | 119, 203 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))) = ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)))) |
| 205 | | eqid 2737 |
. . . . . . . 8
⊢
((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵))) = ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵))) |
| 206 | 1, 2, 3, 10, 20, 4, 16, 205, 14, 22 | miriso 28678 |
. . . . . . 7
⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))) = (𝐵 − (𝑆‘𝐴))) |
| 207 | 204, 206 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴)))) |
| 208 | 207 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴)))) |
| 209 | 1, 2, 3, 125, 132, 126, 133, 130, 208 | tgcgrcomlr 28488 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑆‘𝐴) − 𝐵) = ((𝑆‘(𝑀‘𝐴)) − (𝑀‘𝐵))) |
| 210 | 121 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵))) |
| 211 | 1, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210 | axtg5seg 28473 |
. . 3
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐴 − 𝐵) = ((𝑀‘𝐴) − (𝑀‘𝐵))) |
| 212 | 211 | eqcomd 2743 |
. 2
⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |
| 213 | 124, 212 | pm2.61dane 3029 |
1
⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |