Metamath Proof Explorer

Theorem elplngid

Description: The point R is itself an element of a plane defined by a line A and the 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 elplngid 
|- ( ph -> R e. ( 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 7 eldifad 
 |-  ( ph -> R e. P )
9 eleq1w 
 |-  ( a = c -> ( a e. ( P \ A ) <-> c e. ( P \ A ) ) )
10 eleq1w 
 |-  ( b = d -> ( b e. ( P \ A ) <-> d e. ( P \ A ) ) )
11 9 10 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) <-> ( c e. ( P \ A ) /\ d e. ( P \ A ) ) ) )
12 eleq1w 
 |-  ( t = s -> ( t e. ( a I b ) <-> s e. ( a I b ) ) )
13 12 cbvrexvw 
 |-  ( E. t e. A t e. ( a I b ) <-> E. s e. A s e. ( a I b ) )
14 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a I b ) = ( c I d ) )
15 14 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( s e. ( a I b ) <-> s e. ( c I d ) ) )
16 15 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. A s e. ( a I b ) <-> E. s e. A s e. ( c I d ) ) )
17 13 16 bitrid 
 |-  ( ( a = c /\ b = d ) -> ( E. t e. A t e. ( a I b ) <-> E. s e. A s e. ( c I d ) ) )
18 11 17 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 ) ) ) )
19 18 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 ) ) }
20 7 eldifbd 
 |-  ( ph -> -. R e. A )
21 1 2 3 5 6 8 19 20 hpgid 
 |-  ( ph -> R ( ( hpG ` G ) ` A ) R )
22 21 3mix2d 
 |-  ( ph -> ( R e. A \/ R ( ( hpG ` G ) ` A ) R \/ R { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } R ) )
23 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 ) ) }
24 1 2 3 4 5 6 7 23 8 elplng 
 |-  ( ph -> ( R e. ( A E R ) <-> ( R e. A \/ R ( ( hpG ` G ) ` A ) R \/ R { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } R ) ) )
25 22 24 mpbird 
 |-  ( ph -> R e. ( A E R ) )