Metamath Proof Explorer

Theorem perpln2

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 perpln2 
|- ( ph -> B 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 26 rneqd 
 |-  ( ph -> ran ( perpG ` G ) = ran { <. 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 ) ) } )
28 23 rnssi 
 |-  ran { <. 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 ( ran L X. ran L )
29 27 28 eqsstrdi 
 |-  ( ph -> ran ( perpG ` G ) C_ ran ( ran L X. ran L ) )
30 rnxpss 
 |-  ran ( ran L X. ran L ) C_ ran L
31 29 30 sstrdi 
 |-  ( ph -> ran ( perpG ` G ) C_ ran L )
32 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 ) ) }
33 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 ) ) } ) )
34 32 33 mpbiri 
 |-  ( ph -> Rel ( perpG ` G ) )
35 brrelex12 
 |-  ( ( Rel ( perpG ` G ) /\ A ( perpG ` G ) B ) -> ( A e. _V /\ B e. _V ) )
36 34 3 35 syl2anc 
 |-  ( ph -> ( A e. _V /\ B e. _V ) )
37 36 simpld 
 |-  ( ph -> A e. _V )
38 36 simprd 
 |-  ( ph -> B e. _V )
39 brelrng 
 |-  ( ( A e. _V /\ B e. _V /\ A ( perpG ` G ) B ) -> B e. ran ( perpG ` G ) )
40 37 38 3 39 syl3anc 
 |-  ( ph -> B e. ran ( perpG ` G ) )
41 31 40 sseldd 
 |-  ( ph -> B e. ran L )