Metamath Proof Explorer

Theorem plngcp

Description: The plane defined by a line A and a point R can also be defined using a different point R on the same plane: changes the point used to define the plane. Theorem 9.21 of Schwabhauser p. 74. (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
plngcp.a ⊢ φ → A ∈ ran ⁡ L
plngcp.r ⊢ φ → R ∈ P ∖ A
plngcp.s ⊢ φ → S ∈ A E R ∖ A
Assertion plngcp ⊢ φ → A E R = A E S

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 plngcp.a ⊢ φ → A ∈ ran ⁡ L
7 plngcp.r ⊢ φ → R ∈ P ∖ A
8 plngcp.s ⊢ φ → S ∈ A E R ∖ A
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 1 2 3 4 5 6 7 8 19 plngcplem ⊢ φ → A E R = A E S