Metamath Proof Explorer

Theorem lnssplng

Description: A line defined by two points X and Y , both on a plane H , is entirely contained in H . Theorem 9.25 of Schwabhauser p. 75. (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 )
lnssplng.h 
|- ( ph -> H e. ran E )
lnssplng.x 
|- ( ph -> X e. H )
lnssplng.y 
|- ( ph -> Y e. H )
lnssplng.1 
|- ( ph -> X =/= Y )
Assertion lnssplng 
|- ( ph -> ( ( X L Y ) C_ H /\ E. s e. ( P \ ( X L Y ) ) H = ( ( X L Y ) E s ) ) )

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 lnssplng.h 
 |-  ( ph -> H e. ran E )
7 lnssplng.x 
 |-  ( ph -> X e. H )
8 lnssplng.y 
 |-  ( ph -> Y e. H )
9 lnssplng.1 
 |-  ( ph -> X =/= Y )
10 simpr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> a = ( X L Y ) )
11 5 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> G e. TarskiG )
12 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> a e. ran L )
13 simpllr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> r e. ( P \ a ) )
14 1 2 3 4 11 12 13 elplnglnid 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> a C_ ( a E r ) )
15 10 14 eqsstrrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> ( X L Y ) C_ ( a E r ) )
16 oveq2 
 |-  ( s = r -> ( ( X L Y ) E s ) = ( ( X L Y ) E r ) )
17 16 eqeq2d 
 |-  ( s = r -> ( ( a E r ) = ( ( X L Y ) E s ) <-> ( a E r ) = ( ( X L Y ) E r ) ) )
18 13 eldifad 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> r e. P )
19 13 eldifbd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> -. r e. a )
20 19 10 neleqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> -. r e. ( X L Y ) )
21 18 20 eldifd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> r e. ( P \ ( X L Y ) ) )
22 10 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> ( a E r ) = ( ( X L Y ) E r ) )
23 17 21 22 rspcedvdw 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) )
24 15 23 jca 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a = ( X L Y ) ) -> ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) )
25 5 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> G e. TarskiG )
26 25 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> G e. TarskiG )
27 8 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> Y e. H )
28 simplr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> H = ( a E r ) )
29 27 28 eleqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> Y e. ( a E r ) )
30 29 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> Y e. ( a E r ) )
31 7 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> X e. H )
32 31 28 eleqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> X e. ( a E r ) )
33 32 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> X e. ( a E r ) )
34 9 necomd 
 |-  ( ph -> Y =/= X )
35 34 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> Y =/= X )
36 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> a e. ran L )
37 36 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> a e. ran L )
38 simpllr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> r e. ( P \ a ) )
39 38 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> r e. ( P \ a ) )
40 simplr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> a =/= ( X L Y ) )
41 1 2 3 4 5 6 7 plngrnssp 
 |-  ( ph -> X e. P )
42 1 2 3 4 5 6 8 plngrnssp 
 |-  ( ph -> Y e. P )
43 1 2 3 5 41 42 9 tglinecom 
 |-  ( ph -> ( X L Y ) = ( Y L X ) )
44 43 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> ( X L Y ) = ( Y L X ) )
45 40 44 neeqtrd 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> a =/= ( Y L X ) )
46 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> -. X e. a )
47 1 2 3 4 26 30 33 35 37 39 45 46 lnssplnglem 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> ( ( Y L X ) C_ ( a E r ) /\ E. s e. ( P \ ( Y L X ) ) ( a E r ) = ( ( Y L X ) E s ) ) )
48 43 sseq1d 
 |-  ( ph -> ( ( X L Y ) C_ ( a E r ) <-> ( Y L X ) C_ ( a E r ) ) )
49 43 difeq2d 
 |-  ( ph -> ( P \ ( X L Y ) ) = ( P \ ( Y L X ) ) )
50 43 oveq1d 
 |-  ( ph -> ( ( X L Y ) E s ) = ( ( Y L X ) E s ) )
51 50 eqeq2d 
 |-  ( ph -> ( ( a E r ) = ( ( X L Y ) E s ) <-> ( a E r ) = ( ( Y L X ) E s ) ) )
52 49 51 rexeqbidv 
 |-  ( ph -> ( E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) <-> E. s e. ( P \ ( Y L X ) ) ( a E r ) = ( ( Y L X ) E s ) ) )
53 48 52 anbi12d 
 |-  ( ph -> ( ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) <-> ( ( Y L X ) C_ ( a E r ) /\ E. s e. ( P \ ( Y L X ) ) ( a E r ) = ( ( Y L X ) E s ) ) ) )
54 53 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> ( ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) <-> ( ( Y L X ) C_ ( a E r ) /\ E. s e. ( P \ ( Y L X ) ) ( a E r ) = ( ( Y L X ) E s ) ) ) )
55 47 54 mpbird 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. X e. a ) -> ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) )
56 25 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> G e. TarskiG )
57 32 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> X e. ( a E r ) )
58 29 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> Y e. ( a E r ) )
59 9 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> X =/= Y )
60 59 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> X =/= Y )
61 36 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> a e. ran L )
62 38 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> r e. ( P \ a ) )
63 simplr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> a =/= ( X L Y ) )
64 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> -. Y e. a )
65 1 2 3 4 56 57 58 60 61 62 63 64 lnssplnglem 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ -. Y e. a ) -> ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) )
66 59 neneqd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> -. X = Y )
67 25 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> G e. TarskiG )
68 36 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> a e. ran L )
69 1 2 3 4 25 36 38 32 plngssp 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> X e. P )
70 1 2 3 4 25 36 38 29 plngssp 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> Y e. P )
71 1 2 3 25 69 70 59 tgelrnln 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> ( X L Y ) e. ran L )
72 71 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> ( X L Y ) e. ran L )
73 simplr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> a =/= ( X L Y ) )
74 simprl 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> X e. a )
75 69 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> X e. P )
76 70 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> Y e. P )
77 59 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> X =/= Y )
78 1 2 3 67 75 76 77 tglinerflx1 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> X e. ( X L Y ) )
79 74 78 elind 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> X e. ( a i^i ( X L Y ) ) )
80 simprr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> Y e. a )
81 1 2 3 67 75 76 77 tglinerflx2 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> Y e. ( X L Y ) )
82 80 81 elind 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> Y e. ( a i^i ( X L Y ) ) )
83 1 2 3 67 68 72 73 79 82 tglineineq 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) /\ ( X e. a /\ Y e. a ) ) -> X = Y )
84 66 83 mtand 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> -. ( X e. a /\ Y e. a ) )
85 ianor 
 |-  ( -. ( X e. a /\ Y e. a ) <-> ( -. X e. a \/ -. Y e. a ) )
86 84 85 sylib 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> ( -. X e. a \/ -. Y e. a ) )
87 55 65 86 mpjaodan 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) /\ a =/= ( X L Y ) ) -> ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) )
88 24 87 pm2.61dane 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) )
89 simpr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> H = ( a E r ) )
90 89 sseq2d 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( ( X L Y ) C_ H <-> ( X L Y ) C_ ( a E r ) ) )
91 89 eqeq1d 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( H = ( ( X L Y ) E s ) <-> ( a E r ) = ( ( X L Y ) E s ) ) )
92 91 rexbidv 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( E. s e. ( P \ ( X L Y ) ) H = ( ( X L Y ) E s ) <-> E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) )
93 90 92 anbi12d 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( ( ( X L Y ) C_ H /\ E. s e. ( P \ ( X L Y ) ) H = ( ( X L Y ) E s ) ) <-> ( ( X L Y ) C_ ( a E r ) /\ E. s e. ( P \ ( X L Y ) ) ( a E r ) = ( ( X L Y ) E s ) ) ) )
94 88 93 mpbird 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( ( X L Y ) C_ H /\ E. s e. ( P \ ( X L Y ) ) H = ( ( X L Y ) E s ) ) )
95 1 2 3 4 5 6 isplng 
 |-  ( ph -> E. a e. ran L E. r e. ( P \ a ) H = ( a E r ) )
96 94 95 r19.29vva 
 |-  ( ph -> ( ( X L Y ) C_ H /\ E. s e. ( P \ ( X L Y ) ) H = ( ( X L Y ) E s ) ) )