| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . 3
⊢ (𝑦 = 𝐵 → (𝑅𝐿𝑦) = (𝑅𝐿𝐵)) | 
| 2 | 1 | breq1d 5152 | . 2
⊢ (𝑦 = 𝐵 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))) | 
| 3 |  | oveq2 7440 | . . 3
⊢ (𝑦 = 𝑀 → (𝑅𝐿𝑦) = (𝑅𝐿𝑀)) | 
| 4 | 3 | breq1d 5152 | . 2
⊢ (𝑦 = 𝑀 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝑀)(⟂G‘𝐺)(𝐴𝐿𝐵))) | 
| 5 |  | colperpex.p | . . 3
⊢ 𝑃 = (Base‘𝐺) | 
| 6 |  | colperpex.d | . . 3
⊢  − =
(dist‘𝐺) | 
| 7 |  | colperpex.i | . . 3
⊢ 𝐼 = (Itv‘𝐺) | 
| 8 |  | colperpex.l | . . 3
⊢ 𝐿 = (LineG‘𝐺) | 
| 9 |  | colperpex.g | . . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 10 |  | mideu.1 | . . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 11 |  | mideu.2 | . . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 12 |  | mideulem.1 | . . . 4
⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| 13 | 5, 7, 8, 9, 10, 11, 12 | tgelrnln 28639 | . . 3
⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿) | 
| 14 |  | opphllem.1 | . . 3
⊢ (𝜑 → 𝑅 ∈ 𝑃) | 
| 15 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ≠ 𝐵) | 
| 16 | 15 | neneqd 2944 | . . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝐴 = 𝐵) | 
| 17 |  | mideulem.3 | . . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ 𝑃) | 
| 18 |  | opphllem.3 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅)) | 
| 19 |  | mideulem.6 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂)) | 
| 20 | 8, 9, 19 | perpln2 28720 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿) | 
| 21 | 5, 7, 8, 9, 10, 17, 20 | tglnne 28637 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 𝑂) | 
| 22 | 5, 6, 7, 9, 10, 17, 11, 14, 18, 21 | tgcgrneq 28492 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ≠ 𝑅) | 
| 23 | 22 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ≠ 𝑅) | 
| 24 | 23 | necomd 2995 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ≠ 𝐵) | 
| 25 | 24 | neneqd 2944 | . . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝑅 = 𝐵) | 
| 26 | 16, 25 | jca 511 | . . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵)) | 
| 27 |  | mideu.s | . . . . . 6
⊢ 𝑆 = (pInvG‘𝐺) | 
| 28 | 9 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG) | 
| 29 | 10 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃) | 
| 30 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃) | 
| 31 | 14 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ∈ 𝑃) | 
| 32 |  | mideulem.2 | . . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ 𝑃) | 
| 33 |  | mideulem.5 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵)) | 
| 34 | 8, 9, 33 | perpln2 28720 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄𝐿𝐵) ∈ ran 𝐿) | 
| 35 | 5, 7, 8, 9, 32, 11, 34 | tglnne 28637 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ≠ 𝐵) | 
| 36 | 5, 7, 8, 9, 32, 11, 35 | tglinerflx2 28643 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (𝑄𝐿𝐵)) | 
| 37 | 5, 6, 7, 8, 9, 13,
34, 33 | perpcom 28722 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 38 | 5, 7, 8, 9, 10, 11, 12 | tglinecom 28644 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴)) | 
| 39 | 37, 38 | breqtrd 5168 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐵𝐿𝐴)) | 
| 40 | 5, 6, 7, 8, 9, 32,
11, 36, 10, 39 | perprag 28735 | . . . . . . . . 9
⊢ (𝜑 → 〈“𝑄𝐵𝐴”〉 ∈ (∟G‘𝐺)) | 
| 41 |  | opphllem.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄)) | 
| 42 | 5, 8, 7, 9, 11, 14, 32, 41 | btwncolg3 28566 | . . . . . . . . 9
⊢ (𝜑 → (𝑄 ∈ (𝐵𝐿𝑅) ∨ 𝐵 = 𝑅)) | 
| 43 | 5, 6, 7, 8, 27, 9,
32, 11, 10, 14, 40, 35, 42 | ragcol 28708 | . . . . . . . 8
⊢ (𝜑 → 〈“𝑅𝐵𝐴”〉 ∈ (∟G‘𝐺)) | 
| 44 | 5, 6, 7, 8, 27, 9,
14, 11, 10, 43 | ragcom 28707 | . . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝑅”〉 ∈ (∟G‘𝐺)) | 
| 45 | 44 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 〈“𝐴𝐵𝑅”〉 ∈ (∟G‘𝐺)) | 
| 46 |  | animorrl 982 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 47 | 5, 6, 7, 8, 27, 28, 29, 30, 31, 45, 46 | ragflat3 28715 | . . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝐴 = 𝐵 ∨ 𝑅 = 𝐵)) | 
| 48 |  | oran 991 | . . . . 5
⊢ ((𝐴 = 𝐵 ∨ 𝑅 = 𝐵) ↔ ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵)) | 
| 49 | 47, 48 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵)) | 
| 50 | 26, 49 | pm2.65da 816 | . . 3
⊢ (𝜑 → ¬ 𝑅 ∈ (𝐴𝐿𝐵)) | 
| 51 | 5, 6, 7, 8, 9, 13,
14, 50 | foot 28731 | . 2
⊢ (𝜑 → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 52 | 5, 7, 8, 9, 10, 11, 12 | tglinerflx2 28643 | . 2
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐿𝐵)) | 
| 53 |  | mideulem2.1 | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝑃) | 
| 54 | 12 | neneqd 2944 | . . . . 5
⊢ (𝜑 → ¬ 𝐴 = 𝐵) | 
| 55 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑅𝐿𝑦) = (𝑅𝐿𝐴)) | 
| 56 | 55 | breq1d 5152 | . . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵))) | 
| 57 | 51 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 58 | 5, 7, 8, 9, 10, 11, 12 | tglinerflx1 28642 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵)) | 
| 59 | 58 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐿𝐵)) | 
| 60 | 52 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐵 ∈ (𝐴𝐿𝐵)) | 
| 61 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG) | 
| 62 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ∈ 𝑃) | 
| 63 | 10 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃) | 
| 64 | 50, 54 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → (¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵)) | 
| 65 |  | pm4.56 990 | . . . . . . . . . . . 12
⊢ ((¬
𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 66 | 64, 65 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 67 | 5, 7, 8, 9, 14, 10, 11, 66 | ncolne1 28634 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ≠ 𝐴) | 
| 68 | 67 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝐴) | 
| 69 | 5, 7, 8, 61, 62, 63, 68 | tglinecom 28644 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑅)) | 
| 70 | 68 | necomd 2995 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ≠ 𝑅) | 
| 71 | 17 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ 𝑃) | 
| 72 | 21 | necomd 2995 | . . . . . . . . . 10
⊢ (𝜑 → 𝑂 ≠ 𝐴) | 
| 73 | 72 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝐴) | 
| 74 | 53 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃) | 
| 75 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴) | 
| 76 | 75, 70 | eqnetrd 3007 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ≠ 𝑅) | 
| 77 |  | mideulem2.3 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂)) | 
| 78 | 5, 6, 7, 9, 14, 53, 17, 77 | tgbtwncom 28497 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ (𝑂𝐼𝑅)) | 
| 79 |  | mideulem.4 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ 𝑃) | 
| 80 |  | mideulem.7 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵)) | 
| 81 |  | mideulem2.2 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵)) | 
| 82 | 5, 7, 8, 9, 79, 10, 11, 53, 80, 81 | coltr3 28657 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐵)) | 
| 83 | 12 | necomd 2995 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ≠ 𝐴) | 
| 84 | 83 | neneqd 2944 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ 𝐵 = 𝐴) | 
| 85 | 84 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴) | 
| 86 | 72 | neneqd 2944 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ 𝑂 = 𝐴) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴) | 
| 88 | 85, 87 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴)) | 
| 89 | 9 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG) | 
| 90 | 11 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵 ∈ 𝑃) | 
| 91 | 10 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴 ∈ 𝑃) | 
| 92 | 17 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ 𝑃) | 
| 93 | 5, 7, 8, 9, 11, 10, 83 | tglinerflx2 28643 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐴)) | 
| 94 | 38, 19 | eqbrtrrd 5166 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂)) | 
| 95 | 5, 6, 7, 8, 9, 11,
10, 93, 17, 94 | perprag 28735 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 〈“𝐵𝐴𝑂”〉 ∈ (∟G‘𝐺)) | 
| 96 | 95 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 〈“𝐵𝐴𝑂”〉 ∈ (∟G‘𝐺)) | 
| 97 |  | animorrl 982 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) | 
| 98 | 5, 6, 7, 8, 27, 89, 90, 91, 92, 96, 97 | ragflat3 28715 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴 ∨ 𝑂 = 𝐴)) | 
| 99 |  | oran 991 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 = 𝐴 ∨ 𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴)) | 
| 100 | 98, 99 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴)) | 
| 101 | 88, 100 | pm2.65da 816 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴)) | 
| 102 | 101, 38 | neleqtrrd 2863 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵)) | 
| 103 |  | nelne2 3039 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑋 ≠ 𝑂) | 
| 104 | 82, 102, 103 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ≠ 𝑂) | 
| 105 | 5, 6, 7, 9, 17, 53, 14, 78, 104 | tgbtwnne 28499 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂 ≠ 𝑅) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝑅) | 
| 107 | 106 | necomd 2995 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝑂) | 
| 108 | 77 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐼𝑂)) | 
| 109 | 5, 7, 8, 61, 62, 71, 74, 107, 108 | btwnlng1 28628 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐿𝑂)) | 
| 110 | 5, 7, 8, 61, 74, 62, 71, 76, 109, 107 | lnrot2 28633 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝑋𝐿𝑅)) | 
| 111 | 75 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑋𝐿𝑅) = (𝐴𝐿𝑅)) | 
| 112 | 110, 111 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝐴𝐿𝑅)) | 
| 113 | 5, 7, 8, 61, 63, 62, 70, 71, 73, 112 | tglineelsb2 28641 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑅) = (𝐴𝐿𝑂)) | 
| 114 | 69, 113 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑂)) | 
| 115 | 5, 6, 7, 8, 9, 13,
20, 19 | perpcom 28722 | . . . . . . . 8
⊢ (𝜑 → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 116 | 115 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 117 | 114, 116 | eqbrtrd 5164 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 118 | 13 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵) ∈ ran 𝐿) | 
| 119 | 22 | necomd 2995 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ≠ 𝐵) | 
| 120 | 5, 7, 8, 9, 14, 11, 119 | tgelrnln 28639 | . . . . . . . 8
⊢ (𝜑 → (𝑅𝐿𝐵) ∈ ran 𝐿) | 
| 121 | 120 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵) ∈ ran 𝐿) | 
| 122 | 5, 7, 8, 9, 14, 11, 119 | tglinerflx2 28643 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (𝑅𝐿𝐵)) | 
| 123 | 52, 122 | elind 4199 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝐵))) | 
| 124 | 5, 7, 8, 9, 14, 11, 119 | tglinerflx1 28642 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝐵)) | 
| 125 | 5, 6, 7, 8, 9, 13,
120, 123, 58, 124, 12, 119, 44 | ragperp 28726 | . . . . . . . 8
⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵)) | 
| 126 | 125 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵)) | 
| 127 | 5, 6, 7, 8, 61, 118, 121, 126 | perpcom 28722 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 128 | 56, 2, 57, 59, 60, 117, 127 | reu2eqd 3741 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝐵) | 
| 129 | 54, 128 | mtand 815 | . . . 4
⊢ (𝜑 → ¬ 𝑋 = 𝐴) | 
| 130 | 129 | neqned 2946 | . . 3
⊢ (𝜑 → 𝑋 ≠ 𝐴) | 
| 131 |  | mideulem2.7 | . . 3
⊢ (𝜑 → 𝑀 ∈ 𝑃) | 
| 132 | 130 | necomd 2995 | . . . 4
⊢ (𝜑 → 𝐴 ≠ 𝑋) | 
| 133 |  | eqid 2736 | . . . . 5
⊢ (𝑆‘𝐴) = (𝑆‘𝐴) | 
| 134 |  | eqid 2736 | . . . . 5
⊢ (𝑆‘𝑀) = (𝑆‘𝑀) | 
| 135 | 5, 6, 7, 8, 27, 9,
10, 133, 17 | mircl 28670 | . . . . 5
⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃) | 
| 136 |  | mideulem2.4 | . . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑃) | 
| 137 |  | mideulem2.5 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍)) | 
| 138 | 82 | orcd 873 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 139 | 5, 8, 7, 9, 10, 11, 53, 138 | colcom 28567 | . . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) | 
| 140 | 5, 8, 7, 9, 11, 10, 53, 139 | colrot1 28568 | . . . . . . 7
⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) | 
| 141 | 5, 6, 7, 8, 27, 9,
11, 10, 17, 53, 95, 83, 140 | ragcol 28708 | . . . . . 6
⊢ (𝜑 → 〈“𝑋𝐴𝑂”〉 ∈ (∟G‘𝐺)) | 
| 142 | 5, 6, 7, 8, 27, 9,
53, 10, 17 | israg 28706 | . . . . . 6
⊢ (𝜑 → (〈“𝑋𝐴𝑂”〉 ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))) | 
| 143 | 141, 142 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂))) | 
| 144 |  | mideulem2.6 | . . . . . 6
⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅)) | 
| 145 | 144 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − 𝑍)) | 
| 146 |  | eqidd 2737 | . . . . 5
⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝐴)‘𝑂)) | 
| 147 |  | mideulem2.8 | . . . . . . . 8
⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍)) | 
| 148 | 147 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 → ((𝑆‘𝑀)‘𝑍) = 𝑅) | 
| 149 | 5, 6, 7, 8, 27, 9,
131, 134, 136, 148 | mircom 28672 | . . . . . 6
⊢ (𝜑 → ((𝑆‘𝑀)‘𝑅) = 𝑍) | 
| 150 | 149 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → 𝑍 = ((𝑆‘𝑀)‘𝑅)) | 
| 151 | 5, 6, 7, 8, 27, 9,
133, 134, 17, 135, 53, 14, 136, 10, 131, 78, 137, 143, 145, 146, 150 | krippen 28700 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐴𝐼𝑀)) | 
| 152 | 5, 7, 8, 9, 10, 53, 131, 132, 151 | btwnlng3 28630 | . . 3
⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝑋)) | 
| 153 | 5, 7, 8, 9, 10, 11, 12, 53, 130, 82, 131, 152 | tglineeltr 28640 | . 2
⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝐵)) | 
| 154 | 5, 6, 7, 8, 9, 13,
120, 125 | perpcom 28722 | . 2
⊢ (𝜑 → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 155 |  | nelne2 3039 | . . . . . 6
⊢ ((𝑀 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑀 ≠ 𝑅) | 
| 156 | 153, 50, 155 | syl2anc 584 | . . . . 5
⊢ (𝜑 → 𝑀 ≠ 𝑅) | 
| 157 | 156 | necomd 2995 | . . . 4
⊢ (𝜑 → 𝑅 ≠ 𝑀) | 
| 158 | 5, 7, 8, 9, 14, 131, 157 | tgelrnln 28639 | . . 3
⊢ (𝜑 → (𝑅𝐿𝑀) ∈ ran 𝐿) | 
| 159 | 5, 7, 8, 9, 14, 131, 157 | tglinerflx2 28643 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝑅𝐿𝑀)) | 
| 160 | 153, 159 | elind 4199 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝑀))) | 
| 161 | 5, 7, 8, 9, 14, 131, 157 | tglinerflx1 28642 | . . . 4
⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝑀)) | 
| 162 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝑋) | 
| 163 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐺 ∈ TarskiG) | 
| 164 | 131 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ 𝑃) | 
| 165 | 10 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐴 ∈ 𝑃) | 
| 166 | 17 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑂 ∈ 𝑃) | 
| 167 | 135 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃) | 
| 168 | 143 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂))) | 
| 169 | 162 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑂) = (𝑋 − 𝑂)) | 
| 170 | 162 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑋 − ((𝑆‘𝐴)‘𝑂))) | 
| 171 | 168, 169,
170 | 3eqtr4rd 2787 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑀 − 𝑂)) | 
| 172 | 136 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ∈ 𝑃) | 
| 173 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ∈ 𝑃) | 
| 174 | 147 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 = ((𝑆‘𝑀)‘𝑍)) | 
| 175 | 174 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − ((𝑆‘𝑀)‘𝑍))) | 
| 176 | 5, 6, 7, 8, 27, 163, 164, 134, 172 | mircgr 28666 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝑀)‘𝑍)) = (𝑀 − 𝑍)) | 
| 177 | 175, 176 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − 𝑍)) | 
| 178 | 5, 6, 7, 163, 164, 173, 164, 172, 177 | tgcgrcomlr 28489 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑅 − 𝑀) = (𝑍 − 𝑀)) | 
| 179 | 82 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝐴𝐿𝐵)) | 
| 180 | 162, 179 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝐴𝐿𝐵)) | 
| 181 | 50 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ¬ 𝑅 ∈ (𝐴𝐿𝐵)) | 
| 182 | 180, 181,
155 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ≠ 𝑅) | 
| 183 | 182 | necomd 2995 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ≠ 𝑀) | 
| 184 | 5, 6, 7, 163, 173, 164, 172, 164, 178, 183 | tgcgrneq 28492 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ≠ 𝑀) | 
| 185 | 5, 6, 7, 8, 27, 9,
131, 134, 136 | mirbtwn 28667 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ (((𝑆‘𝑀)‘𝑍)𝐼𝑍)) | 
| 186 | 147 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅𝐼𝑍) = (((𝑆‘𝑀)‘𝑍)𝐼𝑍)) | 
| 187 | 185, 186 | eleqtrrd 2843 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (𝑅𝐼𝑍)) | 
| 188 | 187 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑍)) | 
| 189 | 5, 6, 7, 163, 173, 164, 172, 188 | tgbtwncom 28497 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼𝑅)) | 
| 190 | 137 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍)) | 
| 191 | 162, 190 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍)) | 
| 192 | 5, 6, 7, 163, 167, 164, 172, 191 | tgbtwncom 28497 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼((𝑆‘𝐴)‘𝑂))) | 
| 193 | 77 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝑅𝐼𝑂)) | 
| 194 | 162, 193 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑂)) | 
| 195 | 5, 7, 163, 172, 164, 173, 167, 166, 184, 183, 189, 192, 194 | tgbtwnconn22 28588 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑂)) | 
| 196 | 5, 6, 7, 8, 27, 163, 164, 134, 166, 167, 171, 195 | ismir 28668 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝑀)‘𝑂)) | 
| 197 | 196 | eqcomd 2742 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝑀)‘𝑂) = ((𝑆‘𝐴)‘𝑂)) | 
| 198 | 5, 6, 7, 8, 27, 163, 164, 165, 166, 197 | miduniq1 28695 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝐴) | 
| 199 | 162, 198 | eqtr3d 2778 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 = 𝐴) | 
| 200 | 129, 199 | mtand 815 | . . . . . 6
⊢ (𝜑 → ¬ 𝑀 = 𝑋) | 
| 201 | 200 | neqned 2946 | . . . . 5
⊢ (𝜑 → 𝑀 ≠ 𝑋) | 
| 202 | 201 | necomd 2995 | . . . 4
⊢ (𝜑 → 𝑋 ≠ 𝑀) | 
| 203 | 149 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (𝑋 − ((𝑆‘𝑀)‘𝑅)) = (𝑋 − 𝑍)) | 
| 204 | 203, 144 | eqtr2d 2777 | . . . . 5
⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅))) | 
| 205 | 5, 6, 7, 8, 27, 9,
53, 131, 14 | israg 28706 | . . . . 5
⊢ (𝜑 → (〈“𝑋𝑀𝑅”〉 ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅)))) | 
| 206 | 204, 205 | mpbird 257 | . . . 4
⊢ (𝜑 → 〈“𝑋𝑀𝑅”〉 ∈ (∟G‘𝐺)) | 
| 207 | 5, 6, 7, 8, 9, 13,
158, 160, 82, 161, 202, 157, 206 | ragperp 28726 | . . 3
⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝑀)) | 
| 208 | 5, 6, 7, 8, 9, 13,
158, 207 | perpcom 28722 | . 2
⊢ (𝜑 → (𝑅𝐿𝑀)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 209 | 2, 4, 51, 52, 153, 154, 208 | reu2eqd 3741 | 1
⊢ (𝜑 → 𝐵 = 𝑀) |