Metamath Proof Explorer

Theorem prlngpln4

Description: Building a parallel line conserves planes, i.e. given a line A and a point X not on A , the (unique) parallel B to A through X lies completely within the plane defined by A and X . Theorem 12.14 of Schwabhauser p. 124. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses prlngpln4.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
prlngpln4.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlngpln4.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlngpln4.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
prlngpln4.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
prlngpln4.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
prlngpln4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
prlngpln4.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion prlngpln4 ( 𝜑 → 𝐵 ⊆ 𝐻 )

Proof

Step Hyp Ref Expression
1 prlngpln4.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
2 prlngpln4.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
3 prlngpln4.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 prlngpln4.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
5 prlngpln4.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
6 prlngpln4.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
7 prlngpln4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
8 prlngpln4.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
10 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ⊆ 𝐻 )
11 9 10 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 ⊆ 𝐻 )
12 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∥ 𝐵 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝑋 ∈ 𝐵 )
17 12 1 2 13 14 15 16 prlngpln3 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ⊆ ( 𝐴 𝐸 𝑋 ) )
18 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
19 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐻 ∈ ran 𝐸 )
20 12 2 3 6 prlngrcl1 ⊢ ( 𝜑 → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
22 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝑋 ∈ 𝐻 )
23 12 2 13 14 15 prlngin0 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
26 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
27 25 26 elind ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
28 27 ne0d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
29 28 neneqd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ¬ ( 𝐴 ∩ 𝐵 ) = ∅ )
30 24 29 pm2.65da ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ¬ 𝑋 ∈ 𝐴 )
31 22 30 eldifd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝑋 ∈ ( 𝐻 ∖ 𝐴 ) )
32 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ⊆ 𝐻 )
33 18 12 1 13 19 21 31 32 plng3p ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐻 = ( 𝐴 𝐸 𝑋 ) )
34 17 33 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ⊆ 𝐻 )
35 11 34 pm2.61dane ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )