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 
|- E = ( PlnG ` G )
prlngpln4.p 
|- .|| = ( parlnG ` G )
prlngpln4.g 
|- ( ph -> G e. TarskiG )
prlngpln4.h 
|- ( ph -> H e. ran E )
prlngpln4.a 
|- ( ph -> A C_ H )
prlngpln4.1 
|- ( ph -> A .|| B )
prlngpln4.x 
|- ( ph -> X e. H )
prlngpln4.2 
|- ( ph -> X e. B )
Assertion prlngpln4 
|- ( ph -> B C_ H )

Proof

Step Hyp Ref Expression
1 prlngpln4.e 
 |-  E = ( PlnG ` G )
2 prlngpln4.p 
 |-  .|| = ( parlnG ` G )
3 prlngpln4.g 
 |-  ( ph -> G e. TarskiG )
4 prlngpln4.h 
 |-  ( ph -> H e. ran E )
5 prlngpln4.a 
 |-  ( ph -> A C_ H )
6 prlngpln4.1 
 |-  ( ph -> A .|| B )
7 prlngpln4.x 
 |-  ( ph -> X e. H )
8 prlngpln4.2 
 |-  ( ph -> X e. B )
9 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
10 5 adantr 
 |-  ( ( ph /\ A = B ) -> A C_ H )
11 9 10 eqsstrrd 
 |-  ( ( ph /\ A = B ) -> B C_ H )
12 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
13 3 adantr 
 |-  ( ( ph /\ A =/= B ) -> G e. TarskiG )
14 6 adantr 
 |-  ( ( ph /\ A =/= B ) -> A .|| B )
15 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
16 8 adantr 
 |-  ( ( ph /\ A =/= B ) -> X e. B )
17 12 1 2 13 14 15 16 prlngpln3 
 |-  ( ( ph /\ A =/= B ) -> B C_ ( A E X ) )
18 eqid 
 |-  ( Base ` G ) = ( Base ` G )
19 4 adantr 
 |-  ( ( ph /\ A =/= B ) -> H e. ran E )
20 12 2 3 6 prlngrcl1 
 |-  ( ph -> A e. ran ( LineG ` G ) )
21 20 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. ran ( LineG ` G ) )
22 7 adantr 
 |-  ( ( ph /\ A =/= B ) -> X e. H )
23 12 2 13 14 15 prlngin0 
 |-  ( ( ph /\ A =/= B ) -> ( A i^i B ) = (/) )
24 23 adantr 
 |-  ( ( ( ph /\ A =/= B ) /\ X e. A ) -> ( A i^i B ) = (/) )
25 simpr 
 |-  ( ( ( ph /\ A =/= B ) /\ X e. A ) -> X e. A )
26 8 ad2antrr 
 |-  ( ( ( ph /\ A =/= B ) /\ X e. A ) -> X e. B )
27 25 26 elind 
 |-  ( ( ( ph /\ A =/= B ) /\ X e. A ) -> X e. ( A i^i B ) )
28 27 ne0d 
 |-  ( ( ( ph /\ A =/= B ) /\ X e. A ) -> ( A i^i B ) =/= (/) )
29 28 neneqd 
 |-  ( ( ( ph /\ A =/= B ) /\ X e. A ) -> -. ( A i^i B ) = (/) )
30 24 29 pm2.65da 
 |-  ( ( ph /\ A =/= B ) -> -. X e. A )
31 22 30 eldifd 
 |-  ( ( ph /\ A =/= B ) -> X e. ( H \ A ) )
32 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> A C_ H )
33 18 12 1 13 19 21 31 32 plng3p 
 |-  ( ( ph /\ A =/= B ) -> H = ( A E X ) )
34 17 33 sseqtrrd 
 |-  ( ( ph /\ A =/= B ) -> B C_ H )
35 11 34 pm2.61dane 
 |-  ( ph -> B C_ H )