Metamath Proof Explorer

Theorem plngval

Description: The plane defined by a line A and a point R outside of A . This is defined as the union of 3 parts: the line itself, the open half-plane containing R , and the points opposite to R (see islnopp ). (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 )
plngval.a 
|- ( ph -> A e. ran L )
plngval.r 
|- ( ph -> R e. ( P \ A ) )
Assertion plngval 
|- ( ph -> ( A E R ) = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I 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 plngval.a 
 |-  ( ph -> A e. ran L )
7 plngval.r 
 |-  ( ph -> R e. ( P \ A ) )
8 df-plng 
 |-  PlnG = ( g e. _V |-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) )
9 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
10 9 3 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
11 10 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
12 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
13 12 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
14 13 difeq1d 
 |-  ( g = G -> ( ( Base ` g ) \ a ) = ( P \ a ) )
15 biidd 
 |-  ( g = G -> ( x e. a <-> x e. a ) )
16 fveq2 
 |-  ( g = G -> ( hpG ` g ) = ( hpG ` G ) )
17 16 fveq1d 
 |-  ( g = G -> ( ( hpG ` g ) ` a ) = ( ( hpG ` G ) ` a ) )
18 17 breqd 
 |-  ( g = G -> ( x ( ( hpG ` g ) ` a ) r <-> x ( ( hpG ` G ) ` a ) r ) )
19 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
20 19 2 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
21 20 oveqd 
 |-  ( g = G -> ( x ( Itv ` g ) r ) = ( x I r ) )
22 21 eleq2d 
 |-  ( g = G -> ( t e. ( x ( Itv ` g ) r ) <-> t e. ( x I r ) ) )
23 22 rexbidv 
 |-  ( g = G -> ( E. t e. a t e. ( x ( Itv ` g ) r ) <-> E. t e. a t e. ( x I r ) ) )
24 15 18 23 3orbi123d 
 |-  ( g = G -> ( ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) <-> ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) ) )
25 13 24 rabeqbidv 
 |-  ( g = G -> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } )
26 11 14 25 mpoeq123dv 
 |-  ( g = G -> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) )
27 5 elexd 
 |-  ( ph -> G e. _V )
28 3 fvexi 
 |-  L e. _V
29 28 rnex 
 |-  ran L e. _V
30 29 a1i 
 |-  ( ph -> ran L e. _V )
31 1 fvexi 
 |-  P e. _V
32 31 difexi 
 |-  ( P \ a ) e. _V
33 32 a1i 
 |-  ( ( ph /\ a e. ran L ) -> ( P \ a ) e. _V )
34 30 33 mpoexd 
 |-  ( ph -> ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) e. _V )
35 8 26 27 34 fvmptd3 
 |-  ( ph -> ( PlnG ` G ) = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) )
36 4 35 eqtrid 
 |-  ( ph -> E = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) )
37 7 adantr 
 |-  ( ( ph /\ a = A ) -> R e. ( P \ A ) )
38 difeq2 
 |-  ( a = A -> ( P \ a ) = ( P \ A ) )
39 38 adantl 
 |-  ( ( ph /\ a = A ) -> ( P \ a ) = ( P \ A ) )
40 37 39 eleqtrrd 
 |-  ( ( ph /\ a = A ) -> R e. ( P \ a ) )
41 eqid 
 |-  { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) }
42 31 a1i 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> P e. _V )
43 41 42 rabexd 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } e. _V )
44 eleq2w2 
 |-  ( a = A -> ( x e. a <-> x e. A ) )
45 44 ad2antrl 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( x e. a <-> x e. A ) )
46 eqidd 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> x = x )
47 fveq2 
 |-  ( a = A -> ( ( hpG ` G ) ` a ) = ( ( hpG ` G ) ` A ) )
48 47 ad2antrl 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( ( hpG ` G ) ` a ) = ( ( hpG ` G ) ` A ) )
49 simprr 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> r = R )
50 46 48 49 breq123d 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( x ( ( hpG ` G ) ` a ) r <-> x ( ( hpG ` G ) ` A ) R ) )
51 simprl 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> a = A )
52 49 oveq2d 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( x I r ) = ( x I R ) )
53 52 eleq2d 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( t e. ( x I r ) <-> t e. ( x I R ) ) )
54 51 53 rexeqbidv 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( E. t e. a t e. ( x I r ) <-> E. t e. A t e. ( x I R ) ) )
55 45 50 54 3orbi123d 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> ( ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) <-> ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) ) )
56 55 rabbidv 
 |-  ( ( ph /\ ( a = A /\ r = R ) ) -> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } )
57 6 40 43 56 ovmpodv2 
 |-  ( ph -> ( E = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) -> ( A E R ) = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } ) )
58 36 57 mpd 
 |-  ( ph -> ( A E R ) = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } )