Metamath Proof Explorer

Theorem isperp2

Description: Property for 2 lines A, B, intersecting at a point X to be perpendicular. Item (i) of definition 8.13 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 )
isperp2.b 
|- ( ph -> B e. ran L )
isperp2.x 
|- ( ph -> X e. ( A i^i B ) )
Assertion isperp2 
|- ( ph -> ( A ( perpG ` G ) 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 isperp2.b 
 |-  ( ph -> B e. ran L )
8 isperp2.x 
 |-  ( ph -> X e. ( A i^i B ) )
9 eqidd 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> u = u )
10 5 ad4antr 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> G e. TarskiG )
11 6 ad4antr 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> A e. ran L )
12 7 ad4antr 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> B e. ran L )
13 simp-4r 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> A ( perpG ` G ) B )
14 1 2 3 4 10 11 12 13 perpneq 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> A =/= B )
15 simpllr 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> x e. ( A i^i B ) )
16 8 ad4antr 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> X e. ( A i^i B ) )
17 1 3 4 10 11 12 14 15 16 tglineineq 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> x = X )
18 eqidd 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> v = v )
19 9 17 18 s3eqd 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> <" u x v "> = <" u X v "> )
20 19 eleq1d 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> ( <" u x v "> e. ( raG ` G ) <-> <" u X v "> e. ( raG ` G ) ) )
21 20 biimpd 
 |-  ( ( ( ( ( ph /\ A ( perpG ` G ) B ) /\ x e. ( A i^i B ) ) /\ u e. A ) /\ v e. B ) -> ( <" u x v "> e. ( raG ` G ) -> <" u X v "> e. ( raG ` G ) ) )
22 21 ralimdva 
 |-  ( ( ( ( ph /\ A ( perpG ` G ) 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 ) ) )
23 22 ralimdva 
 |-  ( ( ( ph /\ A ( perpG ` G ) 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 ) ) )
24 23 imp 
 |-  ( ( ( ( ph /\ A ( perpG ` G ) 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 ) )
25 1 2 3 4 5 6 7 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 ) ) )
26 25 biimpa 
 |-  ( ( 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 ) )
27 24 26 r19.29a 
 |-  ( ( ph /\ A ( perpG ` G ) B ) -> A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) )
28 s3eq2 
 |-  ( x = X -> <" u x v "> = <" u X v "> )
29 28 eleq1d 
 |-  ( x = X -> ( <" u x v "> e. ( raG ` G ) <-> <" u X v "> e. ( raG ` G ) ) )
30 29 2ralbidv 
 |-  ( x = X -> ( 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 ) ) )
31 30 rspcev 
 |-  ( ( 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 ) )
32 8 31 sylan 
 |-  ( ( ph /\ 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 ) )
33 25 adantr 
 |-  ( ( ph /\ A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) ) -> ( 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 ) ) )
34 32 33 mpbird 
 |-  ( ( ph /\ A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) ) -> A ( perpG ` G ) B )
35 27 34 impbida 
 |-  ( ph -> ( A ( perpG ` G ) B <-> A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) ) )