Metamath Proof Explorer

Theorem plng3p

Description: If H is a plane containing a line A and a point R not on A , then H is the plane defined by A and R . Theorem 9.26 of Schwabhauser p. 76. See tglinethru for the 2-point line equivalent. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plng3p.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plng3p.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plng3p.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plng3p.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
plng3p.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
plng3p.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
plng3p.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐻 ∖ 𝐴 ) )
plng3p.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
Assertion plng3p ( 𝜑 → 𝐻 = ( 𝐴 𝐸 𝑅 ) )

Proof

Step Hyp Ref Expression
1 plng3p.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plng3p.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 plng3p.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
4 plng3p.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 plng3p.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
6 plng3p.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 plng3p.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐻 ∖ 𝐴 ) )
8 plng3p.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
9 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) )
10 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
11 10 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → ( 𝐴 𝐸 𝑠 ) = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) )
12 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
13 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝐺 ∈ TarskiG )
14 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝐴 ∈ ran 𝐿 )
15 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) )
16 10 difeq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → ( 𝑃 ∖ 𝐴 ) = ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) )
17 15 16 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝑠 ∈ ( 𝑃 ∖ 𝐴 ) )
18 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝑅 ∈ ( 𝐻 ∖ 𝐴 ) )
19 11 9 eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → ( 𝐴 𝐸 𝑠 ) = 𝐻 )
20 19 difeq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → ( ( 𝐴 𝐸 𝑠 ) ∖ 𝐴 ) = ( 𝐻 ∖ 𝐴 ) )
21 18 20 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝑅 ∈ ( ( 𝐴 𝐸 𝑠 ) ∖ 𝐴 ) )
22 1 12 2 3 13 14 17 21 plngcp ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → ( 𝐴 𝐸 𝑠 ) = ( 𝐴 𝐸 𝑅 ) )
23 9 11 22 3eqtr2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) ) ∧ 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) → 𝐻 = ( 𝐴 𝐸 𝑅 ) )
24 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐺 ∈ TarskiG )
25 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐻 ∈ ran 𝐸 )
26 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 ⊆ 𝐻 )
27 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝑃 )
28 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝑃 )
29 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
30 1 12 2 24 27 28 29 tglinerflx1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( 𝑥 𝐿 𝑦 ) )
31 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
32 30 31 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐴 )
33 26 32 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐻 )
34 1 12 2 24 27 28 29 tglinerflx2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( 𝑥 𝐿 𝑦 ) )
35 34 31 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐴 )
36 26 35 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐻 )
37 1 12 2 3 24 25 33 36 29 lnssplng ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 𝐿 𝑦 ) ⊆ 𝐻 ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) ) )
38 37 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑥 𝐿 𝑦 ) ) 𝐻 = ( ( 𝑥 𝐿 𝑦 ) 𝐸 𝑠 ) )
39 23 38 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐻 = ( 𝐴 𝐸 𝑅 ) )
40 39 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐻 = ( 𝐴 𝐸 𝑅 ) )
41 1 12 2 4 6 tgisline ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
42 40 41 r19.29vva ⊢ ( 𝜑 → 𝐻 = ( 𝐴 𝐸 𝑅 ) )