Metamath Proof Explorer

Theorem elplng

Description: Elementhood in the plane defined by a line A and a point R . Definition 9.20 of Schwabhauser p. 74. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
elplng.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
elplng.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
elplng.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
elplng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
Assertion elplng ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) ↔ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 elplng.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 elplng.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
8 elplng.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
9 elplng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 1 2 3 4 5 6 7 plngval ⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )
11 10 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) ↔ 𝑋 ∈ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } ) )
12 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
13 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ↔ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
14 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑅 ) = ( 𝑋 𝐼 𝑅 ) )
15 14 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ↔ 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) )
16 15 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) )
17 12 13 16 3orbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ↔ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) )
18 17 elrab ⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } ↔ ( 𝑋 ∈ 𝑃 ∧ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) )
19 11 18 bitrdi ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) ) )
20 9 biantrurd ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) ) )
21 7 eldifbd ⊢ ( 𝜑 → ¬ 𝑅 ∈ 𝐴 )
22 21 anim1ci ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ( ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) )
23 22 biantrurd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ↔ ( ( ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) )
24 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
25 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝑃 )
26 7 eldifad ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
27 26 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑅 ∈ 𝑃 )
28 1 24 2 8 25 27 islnopp ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ( 𝑋 𝑂 𝑅 ↔ ( ( ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) )
29 23 28 bitr4d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ↔ 𝑋 𝑂 𝑅 ) )
30 29 orbi2d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ( ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ↔ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) )
31 30 pm5.74da ⊢ ( 𝜑 → ( ( ¬ 𝑋 ∈ 𝐴 → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) ↔ ( ¬ 𝑋 ∈ 𝐴 → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) ) )
32 df-or ⊢ ( ( 𝑋 ∈ 𝐴 ∨ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) ↔ ( ¬ 𝑋 ∈ 𝐴 → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) )
33 df-or ⊢ ( ( 𝑋 ∈ 𝐴 ∨ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) ↔ ( ¬ 𝑋 ∈ 𝐴 → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) )
34 31 32 33 3bitr4g ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∨ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) ↔ ( 𝑋 ∈ 𝐴 ∨ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) ) )
35 3orass ⊢ ( ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ↔ ( 𝑋 ∈ 𝐴 ∨ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ) )
36 3orass ⊢ ( ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ↔ ( 𝑋 ∈ 𝐴 ∨ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) )
37 34 35 36 3bitr4g ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑋 𝐼 𝑅 ) ) ↔ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) )
38 19 20 37 3bitr2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) ↔ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑋 𝑂 𝑅 ) ) )