Metamath Proof Explorer

Theorem perpcom

Description: The "perpendicular" relation commutes. Theorem 8.12 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 )
perpcom.1 
|- ( ph -> A ( perpG ` G ) B )
Assertion perpcom 
|- ( ph -> B ( perpG ` G ) A )

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 perpcom.1 
 |-  ( ph -> A ( perpG ` G ) B )
9 incom 
 |-  ( A i^i B ) = ( B i^i A )
10 9 a1i 
 |-  ( ph -> ( A i^i B ) = ( B i^i A ) )
11 ralcom 
 |-  ( A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) <-> A. v e. B A. u e. A <" u x v "> e. ( raG ` G ) )
12 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
13 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> G e. TarskiG )
14 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> A e. ran L )
15 simplrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> u e. A )
16 1 4 3 13 14 15 tglnpt 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> u e. P )
17 simpllr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> x e. ( A i^i B ) )
18 17 elin1d 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> x e. A )
19 1 4 3 13 14 18 tglnpt 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> x e. P )
20 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> B e. ran L )
21 simplrl 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> v e. B )
22 1 4 3 13 20 21 tglnpt 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> v e. P )
23 simpr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> <" u x v "> e. ( raG ` G ) )
24 1 2 3 4 12 13 16 19 22 23 ragcom 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" u x v "> e. ( raG ` G ) ) -> <" v x u "> e. ( raG ` G ) )
25 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> G e. TarskiG )
26 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> B e. ran L )
27 simplrl 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> v e. B )
28 1 4 3 25 26 27 tglnpt 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> v e. P )
29 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> A e. ran L )
30 simpllr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> x e. ( A i^i B ) )
31 30 elin1d 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> x e. A )
32 1 4 3 25 29 31 tglnpt 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> x e. P )
33 simplrr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> u e. A )
34 1 4 3 25 29 33 tglnpt 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> u e. P )
35 simpr 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> <" v x u "> e. ( raG ` G ) )
36 1 2 3 4 12 25 28 32 34 35 ragcom 
 |-  ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) /\ <" v x u "> e. ( raG ` G ) ) -> <" u x v "> e. ( raG ` G ) )
37 24 36 impbida 
 |-  ( ( ( ph /\ x e. ( A i^i B ) ) /\ ( v e. B /\ u e. A ) ) -> ( <" u x v "> e. ( raG ` G ) <-> <" v x u "> e. ( raG ` G ) ) )
38 37 2ralbidva 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> ( A. v e. B A. u e. A <" u x v "> e. ( raG ` G ) <-> A. v e. B A. u e. A <" v x u "> e. ( raG ` G ) ) )
39 11 38 syl5bb 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> ( A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) <-> A. v e. B A. u e. A <" v x u "> e. ( raG ` G ) ) )
40 10 39 rexeqbidva 
 |-  ( ph -> ( E. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) <-> E. x e. ( B i^i A ) A. v e. B A. u e. A <" v x u "> e. ( raG ` G ) ) )
41 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 ) ) )
42 1 2 3 4 5 7 6 isperp 
 |-  ( ph -> ( B ( perpG ` G ) A <-> E. x e. ( B i^i A ) A. v e. B A. u e. A <" v x u "> e. ( raG ` G ) ) )
43 40 41 42 3bitr4d 
 |-  ( ph -> ( A ( perpG ` G ) B <-> B ( perpG ` G ) A ) )
44 8 43 mpbid 
 |-  ( ph -> B ( perpG ` G ) A )