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 
|- P = ( Base ` G )
plng3p.l 
|- L = ( LineG ` G )
plng3p.e 
|- E = ( PlnG ` G )
plng3p.g 
|- ( ph -> G e. TarskiG )
plng3p.h 
|- ( ph -> H e. ran E )
plng3p.a 
|- ( ph -> A e. ran L )
plng3p.r 
|- ( ph -> R e. ( H \ A ) )
plng3p.1 
|- ( ph -> A C_ H )
Assertion plng3p 
|- ( ph -> H = ( A E R ) )

Proof

Step Hyp Ref Expression
1 plng3p.p 
 |-  P = ( Base ` G )
2 plng3p.l 
 |-  L = ( LineG ` G )
3 plng3p.e 
 |-  E = ( PlnG ` G )
4 plng3p.g 
 |-  ( ph -> G e. TarskiG )
5 plng3p.h 
 |-  ( ph -> H e. ran E )
6 plng3p.a 
 |-  ( ph -> A e. ran L )
7 plng3p.r 
 |-  ( ph -> R e. ( H \ A ) )
8 plng3p.1 
 |-  ( ph -> A C_ H )
9 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> H = ( ( x L y ) E s ) )
10 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> A = ( x L y ) )
11 10 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> ( A E s ) = ( ( x L y ) E s ) )
12 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
13 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> G e. TarskiG )
14 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> A e. ran L )
15 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> s e. ( P \ ( x L y ) ) )
16 10 difeq2d 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> ( P \ A ) = ( P \ ( x L y ) ) )
17 15 16 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> s e. ( P \ A ) )
18 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> R e. ( H \ A ) )
19 11 9 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> ( A E s ) = H )
20 19 difeq1d 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> ( ( A E s ) \ A ) = ( H \ A ) )
21 18 20 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> R e. ( ( A E s ) \ A ) )
22 1 12 2 3 13 14 17 21 plngcp 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> ( A E s ) = ( A E R ) )
23 9 11 22 3eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) /\ s e. ( P \ ( x L y ) ) ) /\ H = ( ( x L y ) E s ) ) -> H = ( A E R ) )
24 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> G e. TarskiG )
25 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> H e. ran E )
26 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> A C_ H )
27 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. P )
28 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. P )
29 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> x =/= y )
30 1 12 2 24 27 28 29 tglinerflx1 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. ( x L y ) )
31 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> A = ( x L y ) )
32 30 31 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. A )
33 26 32 sseldd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. H )
34 1 12 2 24 27 28 29 tglinerflx2 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. ( x L y ) )
35 34 31 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. A )
36 26 35 sseldd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. H )
37 1 12 2 3 24 25 33 36 29 lnssplng 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> ( ( x L y ) C_ H /\ E. s e. ( P \ ( x L y ) ) H = ( ( x L y ) E s ) ) )
38 37 simprd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> E. s e. ( P \ ( x L y ) ) H = ( ( x L y ) E s ) )
39 23 38 r19.29a 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ A = ( x L y ) ) /\ x =/= y ) -> H = ( A E R ) )
40 39 anasss 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> H = ( A E R ) )
41 1 12 2 4 6 tgisline 
 |-  ( ph -> E. x e. P E. y e. P ( A = ( x L y ) /\ x =/= y ) )
42 40 41 r19.29vva 
 |-  ( ph -> H = ( A E R ) )