Metamath Proof Explorer

Theorem lnincplng

Description: If two lines A and B intersect, then B is in a plane defined by A and any point of B . Lemma 9.22 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 = ( LineG ` G )
plngval.e 
|- E = ( PlnG ` G )
plngval.g 
|- ( ph -> G e. TarskiG )
lnincplng.a 
|- ( ph -> A e. ran L )
lnincplng.b 
|- ( ph -> B e. ran L )
lnincplng.x 
|- ( ph -> X e. B )
lnincplng.y 
|- ( ph -> Y e. P )
lnincplng.1 
|- ( ph -> X =/= Y )
lnincplng.2 
|- ( ph -> ( A i^i B ) = { Y } )
Assertion lnincplng 
|- ( ph -> B C_ ( A E X ) )

Proof

Step Hyp Ref Expression
1 plngval.p 
 |-  P = ( Base ` G )
2 plngval.i 
 |-  I = ( Itv ` G )
3 plngval.1 
 |-  L = ( LineG ` G )
4 plngval.e 
 |-  E = ( PlnG ` G )
5 plngval.g 
 |-  ( ph -> G e. TarskiG )
6 lnincplng.a 
 |-  ( ph -> A e. ran L )
7 lnincplng.b 
 |-  ( ph -> B e. ran L )
8 lnincplng.x 
 |-  ( ph -> X e. B )
9 lnincplng.y 
 |-  ( ph -> Y e. P )
10 lnincplng.1 
 |-  ( ph -> X =/= Y )
11 lnincplng.2 
 |-  ( ph -> ( A i^i B ) = { Y } )
12 simpr 
 |-  ( ( ( ph /\ z e. B ) /\ z = X ) -> z = X )
13 1 3 2 5 7 8 tglnpt 
 |-  ( ph -> X e. P )
14 10 neneqd 
 |-  ( ph -> -. X = Y )
15 simpr 
 |-  ( ( ph /\ X e. A ) -> X e. A )
16 8 adantr 
 |-  ( ( ph /\ X e. A ) -> X e. B )
17 15 16 elind 
 |-  ( ( ph /\ X e. A ) -> X e. ( A i^i B ) )
18 11 adantr 
 |-  ( ( ph /\ X e. A ) -> ( A i^i B ) = { Y } )
19 17 18 eleqtrd 
 |-  ( ( ph /\ X e. A ) -> X e. { Y } )
20 19 elsnd 
 |-  ( ( ph /\ X e. A ) -> X = Y )
21 14 20 mtand 
 |-  ( ph -> -. X e. A )
22 13 21 eldifd 
 |-  ( ph -> X e. ( P \ A ) )
23 1 2 3 4 5 6 22 elplngid 
 |-  ( ph -> X e. ( A E X ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ z = X ) -> X e. ( A E X ) )
25 12 24 eqeltrd 
 |-  ( ( ( ph /\ z e. B ) /\ z = X ) -> z e. ( A E X ) )
26 simpr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> z = Y )
27 5 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> G e. TarskiG )
28 6 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> A e. ran L )
29 22 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> X e. ( P \ A ) )
30 1 2 3 4 27 28 29 elplnglnid 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> A C_ ( A E X ) )
31 snidg 
 |-  ( Y e. P -> Y e. { Y } )
32 9 31 syl 
 |-  ( ph -> Y e. { Y } )
33 32 11 eleqtrrd 
 |-  ( ph -> Y e. ( A i^i B ) )
34 33 elin1d 
 |-  ( ph -> Y e. A )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> Y e. A )
36 30 35 sseldd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> Y e. ( A E X ) )
37 26 36 eqeltrd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z = Y ) -> z e. ( A E X ) )
38 simpr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> z =/= Y )
39 38 neneqd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> -. z = Y )
40 simpr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z e. A ) -> z e. A )
41 simpllr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> z e. B )
42 41 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z e. A ) -> z e. B )
43 40 42 elind 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z e. A ) -> z e. ( A i^i B ) )
44 11 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z e. A ) -> ( A i^i B ) = { Y } )
45 43 44 eleqtrd 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z e. A ) -> z e. { Y } )
46 45 elsnd 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z e. A ) -> z = Y )
47 39 46 mtand 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> -. z e. A )
48 5 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> G e. TarskiG )
49 6 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> A e. ran L )
50 7 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> B e. ran L )
51 1 3 2 48 50 41 tglnpt 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> z e. P )
52 eleq1w 
 |-  ( a = c -> ( a e. ( P \ A ) <-> c e. ( P \ A ) ) )
53 eleq1w 
 |-  ( b = d -> ( b e. ( P \ A ) <-> d e. ( P \ A ) ) )
54 52 53 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) <-> ( c e. ( P \ A ) /\ d e. ( P \ A ) ) ) )
55 eleq1w 
 |-  ( t = s -> ( t e. ( a I b ) <-> s e. ( a I b ) ) )
56 55 cbvrexvw 
 |-  ( E. t e. A t e. ( a I b ) <-> E. s e. A s e. ( a I b ) )
57 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a I b ) = ( c I d ) )
58 57 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( s e. ( a I b ) <-> s e. ( c I d ) ) )
59 58 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. A s e. ( a I b ) <-> E. s e. A s e. ( c I d ) ) )
60 56 59 bitrid 
 |-  ( ( a = c /\ b = d ) -> ( E. t e. A t e. ( a I b ) <-> E. s e. A s e. ( c I d ) ) )
61 54 60 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) <-> ( ( c e. ( P \ A ) /\ d e. ( P \ A ) ) /\ E. s e. A s e. ( c I d ) ) ) )
62 61 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } = { <. c , d >. | ( ( c e. ( P \ A ) /\ d e. ( P \ A ) ) /\ E. s e. A s e. ( c I d ) ) }
63 13 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> X e. P )
64 34 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> Y e. A )
65 9 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> Y e. P )
66 simplr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> z =/= X )
67 33 elin2d 
 |-  ( ph -> Y e. B )
68 67 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> Y e. B )
69 66 necomd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> X =/= z )
70 8 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> X e. B )
71 1 2 3 48 63 51 69 69 50 70 41 tglinethru 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> B = ( X L z ) )
72 68 71 eleqtrd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> Y e. ( X L z ) )
73 1 2 3 48 51 63 65 66 72 lncom 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> Y e. ( z L X ) )
74 73 orcd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( Y e. ( z L X ) \/ z = X ) )
75 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
76 1 2 3 48 49 51 62 63 64 74 75 colhp 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z ( ( hpG ` G ) ` A ) X <-> ( z ( ( hlG ` G ) ` Y ) X /\ -. z e. A ) ) )
77 47 76 mpbiran2d 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z ( ( hpG ` G ) ` A ) X <-> z ( ( hlG ` G ) ` Y ) X ) )
78 77 biimpar 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ z ( ( hlG ` G ) ` Y ) X ) -> z ( ( hpG ` G ) ` A ) X )
79 eqid 
 |-  ( dist ` G ) = ( dist ` G )
80 51 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> z e. P )
81 63 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> X e. P )
82 64 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> Y e. A )
83 47 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> -. z e. A )
84 21 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> -. X e. A )
85 84 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> -. X e. A )
86 48 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> G e. TarskiG )
87 65 adantr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> Y e. P )
88 simpr 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> Y e. ( X I z ) )
89 1 79 2 86 81 87 80 88 tgbtwncom 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> Y e. ( z I X ) )
90 1 79 2 62 80 81 82 83 85 89 islnoppd 
 |-  ( ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) /\ Y e. ( X I z ) ) -> z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X )
91 1 2 3 5 13 9 10 10 7 8 67 tglinethru 
 |-  ( ph -> B = ( X L Y ) )
92 91 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> B = ( X L Y ) )
93 41 92 eleqtrd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> z e. ( X L Y ) )
94 1 2 75 63 65 51 48 63 3 93 lnhl 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z ( ( hlG ` G ) ` Y ) X \/ Y e. ( X I z ) ) )
95 78 90 94 orim12da 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z ( ( hpG ` G ) ` A ) X \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X ) )
96 95 olcd 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z e. A \/ ( z ( ( hpG ` G ) ` A ) X \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X ) ) )
97 3orass 
 |-  ( ( z e. A \/ z ( ( hpG ` G ) ` A ) X \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X ) <-> ( z e. A \/ ( z ( ( hpG ` G ) ` A ) X \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X ) ) )
98 96 97 sylibr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z e. A \/ z ( ( hpG ` G ) ` A ) X \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X ) )
99 22 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> X e. ( P \ A ) )
100 1 2 3 4 48 49 99 62 51 elplng 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> ( z e. ( A E X ) <-> ( z e. A \/ z ( ( hpG ` G ) ` A ) X \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } X ) ) )
101 98 100 mpbird 
 |-  ( ( ( ( ph /\ z e. B ) /\ z =/= X ) /\ z =/= Y ) -> z e. ( A E X ) )
102 37 101 pm2.61dane 
 |-  ( ( ( ph /\ z e. B ) /\ z =/= X ) -> z e. ( A E X ) )
103 25 102 pm2.61dane 
 |-  ( ( ph /\ z e. B ) -> z e. ( A E X ) )
104 103 ex 
 |-  ( ph -> ( z e. B -> z e. ( A E X ) ) )
105 104 ssrdv 
 |-  ( ph -> B C_ ( A E X ) )