| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | isperp.p | . . 3
⊢ 𝑃 = (Base‘𝐺) | 
| 2 |  | isperp.d | . . 3
⊢  − =
(dist‘𝐺) | 
| 3 |  | isperp.i | . . 3
⊢ 𝐼 = (Itv‘𝐺) | 
| 4 |  | isperp.l | . . 3
⊢ 𝐿 = (LineG‘𝐺) | 
| 5 |  | isperp.g | . . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 6 |  | isperp.a | . . 3
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) | 
| 7 |  | foot.x | . . 3
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 8 |  | foot.y | . . 3
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | footex 28729 | . 2
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | 
| 10 |  | eqid 2737 | . . . . . 6
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) | 
| 11 | 5 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝐺 ∈ TarskiG) | 
| 12 | 7 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝐶 ∈ 𝑃) | 
| 13 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐺 ∈ TarskiG) | 
| 14 | 6 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐴 ∈ ran 𝐿) | 
| 15 |  | simprl 771 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ∈ 𝐴) | 
| 16 | 1, 4, 3, 13, 14, 15 | tglnpt 28557 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ∈ 𝑃) | 
| 17 | 16 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝑥 ∈ 𝑃) | 
| 18 |  | simprr 773 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴) | 
| 19 | 1, 4, 3, 13, 14, 18 | tglnpt 28557 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝑃) | 
| 20 | 19 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝑧 ∈ 𝑃) | 
| 21 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ¬ 𝐶 ∈ 𝐴) | 
| 22 |  | nelne2 3040 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑥 ≠ 𝐶) | 
| 23 | 15, 21, 22 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ≠ 𝐶) | 
| 24 | 23 | necomd 2996 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐶 ≠ 𝑥) | 
| 25 | 24 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝐶 ≠ 𝑥) | 
| 26 | 1, 3, 4, 11, 12, 17, 25 | tglinerflx1 28641 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝐶 ∈ (𝐶𝐿𝑥)) | 
| 27 | 18 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝑧 ∈ 𝐴) | 
| 28 |  | simprl 771 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | 
| 29 | 7 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐶 ∈ 𝑃) | 
| 30 | 1, 3, 4, 13, 29, 16, 24 | tgelrnln 28638 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝐶𝐿𝑥) ∈ ran 𝐿) | 
| 31 | 1, 3, 4, 13, 29, 16, 24 | tglinerflx2 28642 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ∈ (𝐶𝐿𝑥)) | 
| 32 | 31, 15 | elind 4200 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ∈ ((𝐶𝐿𝑥) ∩ 𝐴)) | 
| 33 | 1, 2, 3, 4, 13, 30, 14, 32 | isperp2 28723 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ↔ ∀𝑢 ∈ (𝐶𝐿𝑥)∀𝑣 ∈ 𝐴 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) | 
| 34 | 33 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ↔ ∀𝑢 ∈ (𝐶𝐿𝑥)∀𝑣 ∈ 𝐴 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) | 
| 35 | 28, 34 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → ∀𝑢 ∈ (𝐶𝐿𝑥)∀𝑣 ∈ 𝐴 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) | 
| 36 |  | id 22 | . . . . . . . . . 10
⊢ (𝑢 = 𝐶 → 𝑢 = 𝐶) | 
| 37 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑢 = 𝐶 → 𝑥 = 𝑥) | 
| 38 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑢 = 𝐶 → 𝑣 = 𝑣) | 
| 39 | 36, 37, 38 | s3eqd 14903 | . . . . . . . . 9
⊢ (𝑢 = 𝐶 → 〈“𝑢𝑥𝑣”〉 = 〈“𝐶𝑥𝑣”〉) | 
| 40 | 39 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑢 = 𝐶 → (〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ 〈“𝐶𝑥𝑣”〉 ∈ (∟G‘𝐺))) | 
| 41 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑣 = 𝑧 → 𝐶 = 𝐶) | 
| 42 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑣 = 𝑧 → 𝑥 = 𝑥) | 
| 43 |  | id 22 | . . . . . . . . . 10
⊢ (𝑣 = 𝑧 → 𝑣 = 𝑧) | 
| 44 | 41, 42, 43 | s3eqd 14903 | . . . . . . . . 9
⊢ (𝑣 = 𝑧 → 〈“𝐶𝑥𝑣”〉 = 〈“𝐶𝑥𝑧”〉) | 
| 45 | 44 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑣 = 𝑧 → (〈“𝐶𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ 〈“𝐶𝑥𝑧”〉 ∈ (∟G‘𝐺))) | 
| 46 | 40, 45 | rspc2va 3634 | . . . . . . 7
⊢ (((𝐶 ∈ (𝐶𝐿𝑥) ∧ 𝑧 ∈ 𝐴) ∧ ∀𝑢 ∈ (𝐶𝐿𝑥)∀𝑣 ∈ 𝐴 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 〈“𝐶𝑥𝑧”〉 ∈ (∟G‘𝐺)) | 
| 47 | 26, 27, 35, 46 | syl21anc 838 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 〈“𝐶𝑥𝑧”〉 ∈ (∟G‘𝐺)) | 
| 48 |  | nelne2 3040 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑧 ≠ 𝐶) | 
| 49 | 18, 21, 48 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ≠ 𝐶) | 
| 50 | 49 | necomd 2996 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐶 ≠ 𝑧) | 
| 51 | 50 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝐶 ≠ 𝑧) | 
| 52 | 1, 3, 4, 11, 12, 20, 51 | tglinerflx1 28641 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝐶 ∈ (𝐶𝐿𝑧)) | 
| 53 | 15 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝑥 ∈ 𝐴) | 
| 54 |  | simprr 773 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴) | 
| 55 | 1, 3, 4, 13, 29, 19, 50 | tgelrnln 28638 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝐶𝐿𝑧) ∈ ran 𝐿) | 
| 56 | 1, 3, 4, 13, 29, 19, 50 | tglinerflx2 28642 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ (𝐶𝐿𝑧)) | 
| 57 | 56, 18 | elind 4200 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ ((𝐶𝐿𝑧) ∩ 𝐴)) | 
| 58 | 1, 2, 3, 4, 13, 55, 14, 57 | isperp2 28723 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝐶𝐿𝑧)(⟂G‘𝐺)𝐴 ↔ ∀𝑢 ∈ (𝐶𝐿𝑧)∀𝑣 ∈ 𝐴 〈“𝑢𝑧𝑣”〉 ∈ (∟G‘𝐺))) | 
| 59 | 58 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → ((𝐶𝐿𝑧)(⟂G‘𝐺)𝐴 ↔ ∀𝑢 ∈ (𝐶𝐿𝑧)∀𝑣 ∈ 𝐴 〈“𝑢𝑧𝑣”〉 ∈ (∟G‘𝐺))) | 
| 60 | 54, 59 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → ∀𝑢 ∈ (𝐶𝐿𝑧)∀𝑣 ∈ 𝐴 〈“𝑢𝑧𝑣”〉 ∈ (∟G‘𝐺)) | 
| 61 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑢 = 𝐶 → 𝑧 = 𝑧) | 
| 62 | 36, 61, 38 | s3eqd 14903 | . . . . . . . . 9
⊢ (𝑢 = 𝐶 → 〈“𝑢𝑧𝑣”〉 = 〈“𝐶𝑧𝑣”〉) | 
| 63 | 62 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑢 = 𝐶 → (〈“𝑢𝑧𝑣”〉 ∈ (∟G‘𝐺) ↔ 〈“𝐶𝑧𝑣”〉 ∈ (∟G‘𝐺))) | 
| 64 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑣 = 𝑥 → 𝐶 = 𝐶) | 
| 65 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑣 = 𝑥 → 𝑧 = 𝑧) | 
| 66 |  | id 22 | . . . . . . . . . 10
⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥) | 
| 67 | 64, 65, 66 | s3eqd 14903 | . . . . . . . . 9
⊢ (𝑣 = 𝑥 → 〈“𝐶𝑧𝑣”〉 = 〈“𝐶𝑧𝑥”〉) | 
| 68 | 67 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑣 = 𝑥 → (〈“𝐶𝑧𝑣”〉 ∈ (∟G‘𝐺) ↔ 〈“𝐶𝑧𝑥”〉 ∈ (∟G‘𝐺))) | 
| 69 | 63, 68 | rspc2va 3634 | . . . . . . 7
⊢ (((𝐶 ∈ (𝐶𝐿𝑧) ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑢 ∈ (𝐶𝐿𝑧)∀𝑣 ∈ 𝐴 〈“𝑢𝑧𝑣”〉 ∈ (∟G‘𝐺)) → 〈“𝐶𝑧𝑥”〉 ∈ (∟G‘𝐺)) | 
| 70 | 52, 53, 60, 69 | syl21anc 838 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 〈“𝐶𝑧𝑥”〉 ∈ (∟G‘𝐺)) | 
| 71 | 1, 2, 3, 4, 10, 11, 12, 17, 20, 47, 70 | ragflat 28712 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) → 𝑥 = 𝑧) | 
| 72 | 71 | ex 412 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴) → 𝑥 = 𝑧)) | 
| 73 | 72 | ralrimivva 3202 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴) → 𝑥 = 𝑧)) | 
| 74 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝑧 → (𝐶𝐿𝑥) = (𝐶𝐿𝑧)) | 
| 75 | 74 | breq1d 5153 | . . . 4
⊢ (𝑥 = 𝑧 → ((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ↔ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴)) | 
| 76 | 75 | rmo4 3736 | . . 3
⊢
(∃*𝑥 ∈
𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (((𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ (𝐶𝐿𝑧)(⟂G‘𝐺)𝐴) → 𝑥 = 𝑧)) | 
| 77 | 73, 76 | sylibr 234 | . 2
⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | 
| 78 |  | reu5 3382 | . 2
⊢
(∃!𝑥 ∈
𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ↔ (∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴 ∧ ∃*𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)) | 
| 79 | 9, 77, 78 | sylanbrc 583 | 1
⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) |