Metamath Proof Explorer

Theorem plngrot

Description: The plane defined by a line ( X L Y ) and a point Z is also defined by the line ( Z L Y ) and the point X . See first part of Theorem 9.24 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
plngrot.x ⊢ φ → X ∈ P ∖ Z L Y
plngrot.y ⊢ φ → Y ∈ P
plngrot.z ⊢ φ → Z ∈ P ∖ X L Y
plngrot.1 ⊢ φ → X ≠ Y
Assertion plngrot ⊢ φ → X L Y E Z = Z L Y E X

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 plngrot.x ⊢ φ → X ∈ P ∖ Z L Y
7 plngrot.y ⊢ φ → Y ∈ P
8 plngrot.z ⊢ φ → Z ∈ P ∖ X L Y
9 plngrot.1 ⊢ φ → X ≠ Y
10 eqid ⊢ Itv ⁡ G = Itv ⁡ G
11 eleq1w ⊢ a = c → a ∈ P ∖ X L Y ↔ c ∈ P ∖ X L Y
12 eleq1w ⊢ b = d → b ∈ P ∖ X L Y ↔ d ∈ P ∖ X L Y
13 11 12 bi2anan9 ⊢ a = c ∧ b = d → a ∈ P ∖ X L Y ∧ b ∈ P ∖ X L Y ↔ c ∈ P ∖ X L Y ∧ d ∈ P ∖ X L Y
14 eleq1w ⊢ t = u → t ∈ a Itv ⁡ G b ↔ u ∈ a Itv ⁡ G b
15 14 cbvrexvw ⊢ ∃ t ∈ X L Y t ∈ a Itv ⁡ G b ↔ ∃ u ∈ X L Y u ∈ a Itv ⁡ G b
16 oveq12 ⊢ a = c ∧ b = d → a Itv ⁡ G b = c Itv ⁡ G d
17 16 eleq2d ⊢ a = c ∧ b = d → u ∈ a Itv ⁡ G b ↔ u ∈ c Itv ⁡ G d
18 17 rexbidv ⊢ a = c ∧ b = d → ∃ u ∈ X L Y u ∈ a Itv ⁡ G b ↔ ∃ u ∈ X L Y u ∈ c Itv ⁡ G d
19 15 18 bitrid ⊢ a = c ∧ b = d → ∃ t ∈ X L Y t ∈ a Itv ⁡ G b ↔ ∃ u ∈ X L Y u ∈ c Itv ⁡ G d
20 13 19 anbi12d ⊢ a = c ∧ b = d → a ∈ P ∖ X L Y ∧ b ∈ P ∖ X L Y ∧ ∃ t ∈ X L Y t ∈ a Itv ⁡ G b ↔ c ∈ P ∖ X L Y ∧ d ∈ P ∖ X L Y ∧ ∃ u ∈ X L Y u ∈ c Itv ⁡ G d
21 20 cbvopabv ⊢ a b | a ∈ P ∖ X L Y ∧ b ∈ P ∖ X L Y ∧ ∃ t ∈ X L Y t ∈ a Itv ⁡ G b = c d | c ∈ P ∖ X L Y ∧ d ∈ P ∖ X L Y ∧ ∃ u ∈ X L Y u ∈ c Itv ⁡ G d
22 1 10 3 4 5 6 7 8 9 21 plngrotlem3 ⊢ φ → X L Y E Z ⊆ Z L Y E X
23 6 eldifad ⊢ φ → X ∈ P
24 1 2 3 5 23 7 9 tglinerflx2 ⊢ φ → Y ∈ X L Y
25 8 eldifbd ⊢ φ → ¬ Z ∈ X L Y
26 nelne2 ⊢ Y ∈ X L Y ∧ ¬ Z ∈ X L Y → Y ≠ Z
27 24 25 26 syl2anc ⊢ φ → Y ≠ Z
28 27 necomd ⊢ φ → Z ≠ Y
29 eleq1w ⊢ a = c → a ∈ P ∖ Z L Y ↔ c ∈ P ∖ Z L Y
30 eleq1w ⊢ b = d → b ∈ P ∖ Z L Y ↔ d ∈ P ∖ Z L Y
31 29 30 bi2anan9 ⊢ a = c ∧ b = d → a ∈ P ∖ Z L Y ∧ b ∈ P ∖ Z L Y ↔ c ∈ P ∖ Z L Y ∧ d ∈ P ∖ Z L Y
32 14 cbvrexvw ⊢ ∃ t ∈ Z L Y t ∈ a Itv ⁡ G b ↔ ∃ u ∈ Z L Y u ∈ a Itv ⁡ G b
33 17 rexbidv ⊢ a = c ∧ b = d → ∃ u ∈ Z L Y u ∈ a Itv ⁡ G b ↔ ∃ u ∈ Z L Y u ∈ c Itv ⁡ G d
34 32 33 bitrid ⊢ a = c ∧ b = d → ∃ t ∈ Z L Y t ∈ a Itv ⁡ G b ↔ ∃ u ∈ Z L Y u ∈ c Itv ⁡ G d
35 31 34 anbi12d ⊢ a = c ∧ b = d → a ∈ P ∖ Z L Y ∧ b ∈ P ∖ Z L Y ∧ ∃ t ∈ Z L Y t ∈ a Itv ⁡ G b ↔ c ∈ P ∖ Z L Y ∧ d ∈ P ∖ Z L Y ∧ ∃ u ∈ Z L Y u ∈ c Itv ⁡ G d
36 35 cbvopabv ⊢ a b | a ∈ P ∖ Z L Y ∧ b ∈ P ∖ Z L Y ∧ ∃ t ∈ Z L Y t ∈ a Itv ⁡ G b = c d | c ∈ P ∖ Z L Y ∧ d ∈ P ∖ Z L Y ∧ ∃ u ∈ Z L Y u ∈ c Itv ⁡ G d
37 1 10 3 4 5 8 7 6 28 36 plngrotlem3 ⊢ φ → Z L Y E X ⊆ X L Y E Z
38 22 37 eqssd ⊢ φ → X L Y E Z = Z L Y E X