Metamath Proof Explorer

Theorem isplng

Description: The property of being a plane. (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 )
isplng.h 
|- ( ph -> H e. ran E )
Assertion isplng 
|- ( ph -> E. a e. ran L E. r e. ( P \ a ) H = ( 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 isplng.h 
 |-  ( ph -> H e. ran E )
7 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 ) ) } ) )
8 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
9 8 3 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
10 9 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
11 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
12 11 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
13 12 difeq1d 
 |-  ( g = G -> ( ( Base ` g ) \ a ) = ( P \ a ) )
14 biidd 
 |-  ( g = G -> ( x e. a <-> x e. a ) )
15 fveq2 
 |-  ( g = G -> ( hpG ` g ) = ( hpG ` G ) )
16 15 fveq1d 
 |-  ( g = G -> ( ( hpG ` g ) ` a ) = ( ( hpG ` G ) ` a ) )
17 16 breqd 
 |-  ( g = G -> ( x ( ( hpG ` g ) ` a ) r <-> x ( ( hpG ` G ) ` a ) r ) )
18 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
19 18 2 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
20 19 oveqd 
 |-  ( g = G -> ( x ( Itv ` g ) r ) = ( x I r ) )
21 20 eleq2d 
 |-  ( g = G -> ( t e. ( x ( Itv ` g ) r ) <-> t e. ( x I r ) ) )
22 21 rexbidv 
 |-  ( g = G -> ( E. t e. a t e. ( x ( Itv ` g ) r ) <-> E. t e. a t e. ( x I r ) ) )
23 14 17 22 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 ) ) ) )
24 12 23 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 ) ) } )
25 10 13 24 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 ) ) } ) )
26 5 elexd 
 |-  ( ph -> G e. _V )
27 3 fvexi 
 |-  L e. _V
28 27 rnex 
 |-  ran L e. _V
29 28 a1i 
 |-  ( ph -> ran L e. _V )
30 1 fvexi 
 |-  P e. _V
31 30 difexi 
 |-  ( P \ a ) e. _V
32 31 a1i 
 |-  ( ( ph /\ a e. ran L ) -> ( P \ a ) e. _V )
33 29 32 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 )
34 7 25 26 33 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 ) ) } ) )
35 4 34 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 ) ) } ) )
36 35 rneqd 
 |-  ( ph -> ran E = ran ( 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 6 36 eleqtrd 
 |-  ( ph -> H e. ran ( 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 ) ) } ) )
38 eqid 
 |-  ( 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. 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 ) ) } )
39 30 rabex 
 |-  { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } e. _V
40 38 39 elrnmpo 
 |-  ( H e. ran ( 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. a e. ran L E. r e. ( P \ a ) H = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } )
41 37 40 sylib 
 |-  ( ph -> E. a e. ran L E. r e. ( P \ a ) H = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } )
42 5 ad2antrr 
 |-  ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) -> G e. TarskiG )
43 simplr 
 |-  ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) -> a e. ran L )
44 simpr 
 |-  ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) -> r e. ( P \ a ) )
45 1 2 3 4 42 43 44 plngval 
 |-  ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) -> ( a E r ) = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } )
46 45 eqeq2d 
 |-  ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) -> ( H = ( a E r ) <-> H = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) )
47 46 biimprd 
 |-  ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) -> ( H = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } -> H = ( a E r ) ) )
48 47 anasss 
 |-  ( ( ph /\ ( a e. ran L /\ r e. ( P \ a ) ) ) -> ( H = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } -> H = ( a E r ) ) )
49 48 reximdvva 
 |-  ( ph -> ( E. a e. ran L E. r e. ( P \ a ) H = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } -> E. a e. ran L E. r e. ( P \ a ) H = ( a E r ) ) )
50 41 49 mpd 
 |-  ( ph -> E. a e. ran L E. r e. ( P \ a ) H = ( a E r ) )