Metamath Proof Explorer

Theorem foot

Description: From a point C outside of a line A , there exists a unique point x on A such that ( C L x ) is perpendicular to A . That point is called the foot from C on A . Theorem 8.18 of Schwabhauser p. 60. (Contributed by Thierry Arnoux, 19-Oct-2019)

Ref Expression
Hypotheses isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
foot.x ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
foot.y ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
Assertion foot ( 𝜑 → ∃! 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )

Proof

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