Metamath Proof Explorer

Theorem elplngid

Description: The point R is itself an element of a plane defined by a line A and the point R . (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ P = Base G
plngval.i ⊢ I = Itv ⁡ G
plngval.1 ⊢ L = Line 𝒢 ⁡ G
plngval.e No typesetting found for |- E = ( PlnG ` G ) with typecode |-
plngval.g ⊢ φ → G ∈ 𝒢 Tarski
elplng.a ⊢ φ → A ∈ ran ⁡ L
elplng.r ⊢ φ → R ∈ P ∖ A
Assertion elplngid ⊢ φ → R ∈ A E R

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ P = Base G
2 plngval.i ⊢ I = Itv ⁡ G
3 plngval.1 ⊢ L = Line 𝒢 ⁡ G
4 plngval.e Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
5 plngval.g ⊢ φ → G ∈ 𝒢 Tarski
6 elplng.a ⊢ φ → A ∈ ran ⁡ L
7 elplng.r ⊢ φ → R ∈ P ∖ A
8 7 eldifad ⊢ φ → R ∈ P
9 eleq1w ⊢ a = c → a ∈ P ∖ A ↔ c ∈ P ∖ A
10 eleq1w ⊢ b = d → b ∈ P ∖ A ↔ d ∈ P ∖ A
11 9 10 bi2anan9 ⊢ a = c ∧ b = d → a ∈ P ∖ A ∧ b ∈ P ∖ A ↔ c ∈ P ∖ A ∧ d ∈ P ∖ A
12 eleq1w ⊢ t = s → t ∈ a I b ↔ s ∈ a I b
13 12 cbvrexvw ⊢ ∃ t ∈ A t ∈ a I b ↔ ∃ s ∈ A s ∈ a I b
14 oveq12 ⊢ a = c ∧ b = d → a I b = c I d
15 14 eleq2d ⊢ a = c ∧ b = d → s ∈ a I b ↔ s ∈ c I d
16 15 rexbidv ⊢ a = c ∧ b = d → ∃ s ∈ A s ∈ a I b ↔ ∃ s ∈ A s ∈ c I d
17 13 16 bitrid ⊢ a = c ∧ b = d → ∃ t ∈ A t ∈ a I b ↔ ∃ s ∈ A s ∈ c I d
18 11 17 anbi12d ⊢ a = c ∧ b = d → a ∈ P ∖ A ∧ b ∈ P ∖ A ∧ ∃ t ∈ A t ∈ a I b ↔ c ∈ P ∖ A ∧ d ∈ P ∖ A ∧ ∃ s ∈ A s ∈ c I d
19 18 cbvopabv ⊢ a b | a ∈ P ∖ A ∧ b ∈ P ∖ A ∧ ∃ t ∈ A t ∈ a I b = c d | c ∈ P ∖ A ∧ d ∈ P ∖ A ∧ ∃ s ∈ A s ∈ c I d
20 7 eldifbd ⊢ φ → ¬ R ∈ A
21 1 2 3 5 6 8 19 20 hpgid ⊢ φ → R hp 𝒢 ⁡ G ⁡ A R
22 21 3mix2d ⊢ φ → R ∈ A ∨ R hp 𝒢 ⁡ G ⁡ A R ∨ R a b | a ∈ P ∖ A ∧ b ∈ P ∖ A ∧ ∃ t ∈ A t ∈ a I b R
23 eqid ⊢ a b | a ∈ P ∖ A ∧ b ∈ P ∖ A ∧ ∃ t ∈ A t ∈ a I b = a b | a ∈ P ∖ A ∧ b ∈ P ∖ A ∧ ∃ t ∈ A t ∈ a I b
24 1 2 3 4 5 6 7 23 8 elplng ⊢ φ → R ∈ A E R ↔ R ∈ A ∨ R hp 𝒢 ⁡ G ⁡ A R ∨ R a b | a ∈ P ∖ A ∧ b ∈ P ∖ A ∧ ∃ t ∈ A t ∈ a I b R
25 22 24 mpbird ⊢ φ → R ∈ A E R