Metamath Proof Explorer

Theorem isperp

Description: Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019)

Ref Expression
Hypotheses isperp.p 
|- P = ( Base ` G )
isperp.d 
|- .- = ( dist ` G )
isperp.i 
|- I = ( Itv ` G )
isperp.l 
|- L = ( LineG ` G )
isperp.g 
|- ( ph -> G e. TarskiG )
isperp.a 
|- ( ph -> A e. ran L )
isperp.b 
|- ( ph -> B e. ran L )
Assertion isperp 
|- ( ph -> ( A ( perpG ` G ) B <-> E. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) )

Proof

Step Hyp Ref Expression
1 isperp.p 
 |-  P = ( Base ` G )
2 isperp.d 
 |-  .- = ( dist ` G )
3 isperp.i 
 |-  I = ( Itv ` G )
4 isperp.l 
 |-  L = ( LineG ` G )
5 isperp.g 
 |-  ( ph -> G e. TarskiG )
6 isperp.a 
 |-  ( ph -> A e. ran L )
7 isperp.b 
 |-  ( ph -> B e. ran L )
8 df-br 
 |-  ( A ( perpG ` G ) B <-> <. A , B >. e. ( perpG ` G ) )
9 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 ) ) } )
10 simpr 
 |-  ( ( ph /\ g = G ) -> g = G )
11 10 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( LineG ` g ) = ( LineG ` G ) )
12 11 4 eqtr4di 
 |-  ( ( ph /\ g = G ) -> ( LineG ` g ) = L )
13 12 rneqd 
 |-  ( ( ph /\ g = G ) -> ran ( LineG ` g ) = ran L )
14 13 eleq2d 
 |-  ( ( ph /\ g = G ) -> ( a e. ran ( LineG ` g ) <-> a e. ran L ) )
15 13 eleq2d 
 |-  ( ( ph /\ g = G ) -> ( b e. ran ( LineG ` g ) <-> b e. ran L ) )
16 14 15 anbi12d 
 |-  ( ( ph /\ g = G ) -> ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) <-> ( a e. ran L /\ b e. ran L ) ) )
17 10 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( raG ` g ) = ( raG ` G ) )
18 17 eleq2d 
 |-  ( ( ph /\ g = G ) -> ( <" u x v "> e. ( raG ` g ) <-> <" u x v "> e. ( raG ` G ) ) )
19 18 ralbidv 
 |-  ( ( ph /\ g = G ) -> ( A. v e. b <" u x v "> e. ( raG ` g ) <-> A. v e. b <" u x v "> e. ( raG ` G ) ) )
20 19 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 ) ) )
21 16 20 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 ) ) ) )
22 21 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 ) ) } )
23 5 elexd 
 |-  ( ph -> G e. _V )
24 4 fvexi 
 |-  L e. _V
25 rnexg 
 |-  ( L e. _V -> ran L e. _V )
26 24 25 mp1i 
 |-  ( ph -> ran L e. _V )
27 26 26 xpexd 
 |-  ( ph -> ( ran L X. ran L ) e. _V )
28 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 )
29 28 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 ) )
30 27 29 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 )
31 9 22 23 30 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 ) ) } )
32 31 eleq2d 
 |-  ( ph -> ( <. A , B >. e. ( perpG ` G ) <-> <. A , B >. e. { <. 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 8 32 syl5bb 
 |-  ( ph -> ( A ( perpG ` G ) B <-> <. A , B >. e. { <. 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 ineq12 
 |-  ( ( a = A /\ b = B ) -> ( a i^i b ) = ( A i^i B ) )
35 simpll 
 |-  ( ( ( a = A /\ b = B ) /\ x e. ( a i^i b ) ) -> a = A )
36 simpllr 
 |-  ( ( ( ( a = A /\ b = B ) /\ x e. ( a i^i b ) ) /\ u e. a ) -> b = B )
37 36 raleqdv 
 |-  ( ( ( ( a = A /\ b = B ) /\ x e. ( a i^i b ) ) /\ u e. a ) -> ( A. v e. b <" u x v "> e. ( raG ` G ) <-> A. v e. B <" u x v "> e. ( raG ` G ) ) )
38 35 37 raleqbidva 
 |-  ( ( ( a = A /\ b = B ) /\ x e. ( a i^i b ) ) -> ( A. u e. a A. v e. b <" u x v "> e. ( raG ` G ) <-> A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) )
39 34 38 rexeqbidva 
 |-  ( ( a = A /\ b = B ) -> ( 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 ) ) )
40 39 opelopab2a 
 |-  ( ( A e. ran L /\ B e. ran L ) -> ( <. A , B >. e. { <. 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. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) )
41 6 7 40 syl2anc 
 |-  ( ph -> ( <. A , B >. e. { <. 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. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) )
42 33 41 bitrd 
 |-  ( ph -> ( A ( perpG ` G ) B <-> E. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) )