Metamath Proof Explorer

Theorem perpln1

Description: Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses perpln.l 
|- L = ( LineG ` G )
perpln.1 
|- ( ph -> G e. TarskiG )
perpln.2 
|- ( ph -> A ( perpG ` G ) B )
Assertion perpln1 
|- ( ph -> A e. ran L )

Proof

Step Hyp Ref Expression
1 perpln.l 
 |-  L = ( LineG ` G )
2 perpln.1 
 |-  ( ph -> G e. TarskiG )
3 perpln.2 
 |-  ( ph -> A ( perpG ` G ) B )
4 df-perpg 
 |-  perpG = ( 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. ( raG ` g ) ) } )
5 simpr 
 |-  ( ( ph /\ g = G ) -> g = G )
6 5 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( LineG ` g ) = ( LineG ` G ) )
7 6 1 eqtr4di 
 |-  ( ( ph /\ g = G ) -> ( LineG ` g ) = L )
8 7 rneqd 
 |-  ( ( ph /\ g = G ) -> ran ( LineG ` g ) = ran L )
9 8 eleq2d 
 |-  ( ( ph /\ g = G ) -> ( a e. ran ( LineG ` g ) <-> a e. ran L ) )
10 8 eleq2d 
 |-  ( ( ph /\ g = G ) -> ( b e. ran ( LineG ` g ) <-> b e. ran L ) )
11 9 10 anbi12d 
 |-  ( ( ph /\ g = G ) -> ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) <-> ( a e. ran L /\ b e. ran L ) ) )
12 5 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( raG ` g ) = ( raG ` G ) )
13 12 eleq2d 
 |-  ( ( ph /\ g = G ) -> ( <" u x v "> e. ( raG ` g ) <-> <" u x v "> e. ( raG ` G ) ) )
14 13 ralbidv 
 |-  ( ( ph /\ g = G ) -> ( A. v e. b <" u x v "> e. ( raG ` g ) <-> A. v e. b <" u x v "> e. ( raG ` G ) ) )
15 14 rexralbidv 
 |-  ( ( ph /\ g = G ) -> ( E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. ( raG ` g ) <-> E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. ( raG ` G ) ) )
16 11 15 anbi12d 
 |-  ( ( 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. ( raG ` 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. ( raG ` G ) ) ) )
17 16 opabbidv 
 |-  ( ( 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. ( raG ` 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. ( raG ` G ) ) } )
18 2 elexd 
 |-  ( ph -> G e. _V )
19 1 fvexi 
 |-  L e. _V
20 rnexg 
 |-  ( L e. _V -> ran L e. _V )
21 19 20 mp1i 
 |-  ( ph -> ran L e. _V )
22 21 21 xpexd 
 |-  ( ph -> ( ran L X. ran L ) e. _V )
23 opabssxp 
 |-  { <. 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. ( raG ` G ) ) } C_ ( ran L X. ran L )
24 23 a1i 
 |-  ( 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. ( raG ` G ) ) } C_ ( ran L X. ran L ) )
25 22 24 ssexd 
 |-  ( 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. ( raG ` G ) ) } e. _V )
26 4 17 18 25 fvmptd2 
 |-  ( ph -> ( perpG ` 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. ( raG ` G ) ) } )
27 anass 
 |-  ( ( ( 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. ( raG ` 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. ( raG ` G ) ) ) )
28 27 opabbii 
 |-  { <. 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. ( raG ` 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. ( raG ` G ) ) ) }
29 26 28 eqtrdi 
 |-  ( ph -> ( perpG ` 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. ( raG ` G ) ) ) } )
30 29 dmeqd 
 |-  ( ph -> dom ( perpG ` 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. ( raG ` G ) ) ) } )
31 dmopabss 
 |-  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. ( raG ` G ) ) ) } C_ ran L
32 30 31 eqsstrdi 
 |-  ( ph -> dom ( perpG ` G ) C_ ran L )
33 relopabv 
 |-  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. ( raG ` G ) ) }
34 26 releqd 
 |-  ( ph -> ( Rel ( perpG ` 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. ( raG ` G ) ) } ) )
35 33 34 mpbiri 
 |-  ( ph -> Rel ( perpG ` G ) )
36 brrelex12 
 |-  ( ( Rel ( perpG ` G ) /\ A ( perpG ` G ) B ) -> ( A e. _V /\ B e. _V ) )
37 35 3 36 syl2anc 
 |-  ( ph -> ( A e. _V /\ B e. _V ) )
38 37 simpld 
 |-  ( ph -> A e. _V )
39 37 simprd 
 |-  ( ph -> B e. _V )
40 breldmg 
 |-  ( ( A e. _V /\ B e. _V /\ A ( perpG ` G ) B ) -> A e. dom ( perpG ` G ) )
41 38 39 3 40 syl3anc 
 |-  ( ph -> A e. dom ( perpG ` G ) )
42 32 41 sseldd 
 |-  ( ph -> A e. ran L )