MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  perpln1 Structured version   Unicode version

Theorem perpln1 24697
Description: Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
Hypotheses
Ref Expression
perpln.l  |-  L  =  (LineG `  G )
perpln.1  |-  ( ph  ->  G  e. TarskiG )
perpln.2  |-  ( ph  ->  A (⟂G `  G
) B )
Assertion
Ref Expression
perpln1  |-  ( ph  ->  A  e.  ran  L
)

Proof of Theorem perpln1
Dummy variables  a 
b  g  u  v  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-perpg 24683 . . . . . . 7  |- ⟂G  =  ( g  e.  _V  |->  {
<. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g
) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
) } )
21a1i 11 . . . . . 6  |-  ( ph  -> ⟂G  =  ( g  e. 
_V  |->  { <. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g ) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g
) ) } ) )
3 simpr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  g  =  G )  ->  g  =  G )
43fveq2d 5829 . . . . . . . . . . . 12  |-  ( (
ph  /\  g  =  G )  ->  (LineG `  g )  =  (LineG `  G ) )
5 perpln.l . . . . . . . . . . . 12  |-  L  =  (LineG `  G )
64, 5syl6eqr 2480 . . . . . . . . . . 11  |-  ( (
ph  /\  g  =  G )  ->  (LineG `  g )  =  L )
76rneqd 5024 . . . . . . . . . 10  |-  ( (
ph  /\  g  =  G )  ->  ran  (LineG `  g )  =  ran  L )
87eleq2d 2491 . . . . . . . . 9  |-  ( (
ph  /\  g  =  G )  ->  (
a  e.  ran  (LineG `  g )  <->  a  e.  ran  L ) )
97eleq2d 2491 . . . . . . . . 9  |-  ( (
ph  /\  g  =  G )  ->  (
b  e.  ran  (LineG `  g )  <->  b  e.  ran  L ) )
108, 9anbi12d 715 . . . . . . . 8  |-  ( (
ph  /\  g  =  G )  ->  (
( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g ) )  <->  ( a  e.  ran  L  /\  b  e.  ran  L ) ) )
113fveq2d 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  g  =  G )  ->  (∟G `  g )  =  (∟G `  G ) )
1211eleq2d 2491 . . . . . . . . . 10  |-  ( (
ph  /\  g  =  G )  ->  ( <" u x v ">  e.  (∟G `  g )  <->  <" u x v ">  e.  (∟G `  G )
) )
1312ralbidv 2804 . . . . . . . . 9  |-  ( (
ph  /\  g  =  G )  ->  ( A. v  e.  b  <" u x v ">  e.  (∟G `  g )  <->  A. v  e.  b  <" u x v ">  e.  (∟G `  G )
) )
1413rexralbidv 2886 . . . . . . . 8  |-  ( (
ph  /\  g  =  G )  ->  ( E. x  e.  (
a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )  <->  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) )
1510, 14anbi12d 715 . . . . . . 7  |-  ( (
ph  /\  g  =  G )  ->  (
( ( a  e. 
ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g ) )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g ) )  <-> 
( ( a  e. 
ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G
) ) ) )
1615opabbidv 4430 . . . . . 6  |-  ( (
ph  /\  g  =  G )  ->  { <. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g ) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g
) ) }  =  { <. a ,  b
>.  |  ( (
a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) } )
17 perpln.1 . . . . . . 7  |-  ( ph  ->  G  e. TarskiG )
18 elex 3031 . . . . . . 7  |-  ( G  e. TarskiG  ->  G  e.  _V )
1917, 18syl 17 . . . . . 6  |-  ( ph  ->  G  e.  _V )
20 fvex 5835 . . . . . . . . . 10  |-  (LineG `  G )  e.  _V
215, 20eqeltri 2502 . . . . . . . . 9  |-  L  e. 
_V
22 rnexg 6683 . . . . . . . . 9  |-  ( L  e.  _V  ->  ran  L  e.  _V )
2321, 22mp1i 13 . . . . . . . 8  |-  ( ph  ->  ran  L  e.  _V )
24 xpexg 6551 . . . . . . . 8  |-  ( ( ran  L  e.  _V  /\ 
ran  L  e.  _V )  ->  ( ran  L  X.  ran  L )  e. 
_V )
2523, 23, 24syl2anc 665 . . . . . . 7  |-  ( ph  ->  ( ran  L  X.  ran  L )  e.  _V )
26 opabssxp 4871 . . . . . . . 8  |-  { <. a ,  b >.  |  ( ( a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) }  C_  ( ran  L  X.  ran  L )
2726a1i 11 . . . . . . 7  |-  ( ph  ->  { <. a ,  b
>.  |  ( (
a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) }  C_  ( ran  L  X.  ran  L ) )
2825, 27ssexd 4514 . . . . . 6  |-  ( ph  ->  { <. a ,  b
>.  |  ( (
a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) }  e.  _V )
292, 16, 19, 28fvmptd 5914 . . . . 5  |-  ( ph  ->  (⟂G `  G )  =  { <. a ,  b
>.  |  ( (
a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) } )
30 anass 653 . . . . . 6  |-  ( ( ( a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) )  <-> 
( a  e.  ran  L  /\  ( b  e. 
ran  L  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) ) )
3130opabbii 4431 . . . . 5  |-  { <. a ,  b >.  |  ( ( a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) }  =  { <. a ,  b >.  |  ( a  e.  ran  L  /\  ( b  e.  ran  L  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) ) }
3229, 31syl6eq 2478 . . . 4  |-  ( ph  ->  (⟂G `  G )  =  { <. a ,  b
>.  |  ( a  e.  ran  L  /\  (
b  e.  ran  L  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a 
A. v  e.  b 
<" u x v ">  e.  (∟G `  G ) ) ) } )
3332dmeqd 4999 . . 3  |-  ( ph  ->  dom  (⟂G `  G )  =  dom  { <. a ,  b >.  |  ( a  e.  ran  L  /\  ( b  e.  ran  L  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) ) } )
34 dmopabss 5008 . . 3  |-  dom  { <. a ,  b >.  |  ( a  e. 
ran  L  /\  (
b  e.  ran  L  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a 
A. v  e.  b 
<" u x v ">  e.  (∟G `  G ) ) ) }  C_  ran  L
3533, 34syl6eqss 3457 . 2  |-  ( ph  ->  dom  (⟂G `  G )  C_ 
ran  L )
36 relopab 4922 . . . . . 6  |-  Rel  { <. a ,  b >.  |  ( ( a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) }
3729releqd 4881 . . . . . 6  |-  ( ph  ->  ( Rel  (⟂G `  G
)  <->  Rel  { <. a ,  b >.  |  ( ( a  e.  ran  L  /\  b  e.  ran  L )  /\  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  G ) ) } ) )
3836, 37mpbiri 236 . . . . 5  |-  ( ph  ->  Rel  (⟂G `  G )
)
39 perpln.2 . . . . 5  |-  ( ph  ->  A (⟂G `  G
) B )
40 brrelex12 4834 . . . . 5  |-  ( ( Rel  (⟂G `  G )  /\  A (⟂G `  G
) B )  -> 
( A  e.  _V  /\  B  e.  _V )
)
4138, 39, 40syl2anc 665 . . . 4  |-  ( ph  ->  ( A  e.  _V  /\  B  e.  _V )
)
4241simpld 460 . . 3  |-  ( ph  ->  A  e.  _V )
4341simprd 464 . . 3  |-  ( ph  ->  B  e.  _V )
44 breldmg 5002 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V  /\  A
(⟂G `  G ) B )  ->  A  e.  dom  (⟂G `  G )
)
4542, 43, 39, 44syl3anc 1264 . 2  |-  ( ph  ->  A  e.  dom  (⟂G `  G ) )
4635, 45sseldd 3408 1  |-  ( ph  ->  A  e.  ran  L
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2714   E.wrex 2715   _Vcvv 3022    i^i cin 3378    C_ wss 3379   class class class wbr 4366   {copab 4424    |-> cmpt 4425    X. cxp 4794   dom cdm 4796   ran crn 4797   Rel wrel 4801   ` cfv 5544   <"cs3 12884  TarskiGcstrkg 24420  LineGclng 24427  ∟Gcrag 24680  ⟂Gcperpg 24682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-iota 5508  df-fun 5546  df-fv 5552  df-perpg 24683
This theorem is referenced by:  footne  24707  footeq  24708  perpdragALT  24711  perpdrag  24712  colperp  24713  midex  24721  opphl  24738  lmieu  24768  lnperpex  24787  trgcopy  24788
  Copyright terms: Public domain W3C validator