Metamath Proof Explorer

Theorem elplnglnid

Description: The line A itself is a subset of a plane defined by the line A and a point R . (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 )
elplng.a 
|- ( ph -> A e. ran L )
elplng.r 
|- ( ph -> R e. ( P \ A ) )
Assertion elplnglnid 
|- ( ph -> A C_ ( A E R ) )

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 elplng.a 
 |-  ( ph -> A e. ran L )
7 elplng.r 
 |-  ( ph -> R e. ( P \ A ) )
8 simpr 
 |-  ( ( ph /\ z e. A ) -> z e. A )
9 8 3mix1d 
 |-  ( ( ph /\ z e. A ) -> ( z e. A \/ z ( ( hpG ` G ) ` A ) R \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } R ) )
10 5 adantr 
 |-  ( ( ph /\ z e. A ) -> G e. TarskiG )
11 6 adantr 
 |-  ( ( ph /\ z e. A ) -> A e. ran L )
12 7 adantr 
 |-  ( ( ph /\ z e. A ) -> R e. ( P \ A ) )
13 eqid 
 |-  { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
14 1 3 2 10 11 8 tglnpt 
 |-  ( ( ph /\ z e. A ) -> z e. P )
15 1 2 3 4 10 11 12 13 14 elplng 
 |-  ( ( ph /\ z e. A ) -> ( z e. ( A E R ) <-> ( z e. A \/ z ( ( hpG ` G ) ` A ) R \/ z { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } R ) ) )
16 9 15 mpbird 
 |-  ( ( ph /\ z e. A ) -> z e. ( A E R ) )
17 16 ex 
 |-  ( ph -> ( z e. A -> z e. ( A E R ) ) )
18 17 ssrdv 
 |-  ( ph -> A C_ ( A E R ) )