Metamath Proof Explorer

Theorem perpneq

Description: Two perpendicular lines are different. Theorem 8.14 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 18-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 perpneq 
|- ( ph -> A =/= B )

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 5 adantr 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> G e. TarskiG )
10 9 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> G e. TarskiG )
11 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> G e. TarskiG )
12 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> A e. ran L )
13 simpr 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> x e. ( A i^i B ) )
14 13 elin1d 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> x e. A )
15 14 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> x e. A )
16 1 4 3 11 12 15 tglnpt 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> x e. P )
17 16 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> x e. P )
18 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> B e. ran L )
19 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> v e. B )
20 1 4 3 11 18 19 tglnpt 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> v e. P )
21 20 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> v e. P )
22 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> u e. A )
23 1 4 3 11 12 22 tglnpt 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> u e. P )
24 23 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> u e. P )
25 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
26 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> u e. A )
27 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> v e. B )
28 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) )
29 id 
 |-  ( y = u -> y = u )
30 eqidd 
 |-  ( y = u -> x = x )
31 eqidd 
 |-  ( y = u -> z = z )
32 29 30 31 s3eqd 
 |-  ( y = u -> <" y x z "> = <" u x z "> )
33 32 eleq1d 
 |-  ( y = u -> ( <" y x z "> e. ( raG ` G ) <-> <" u x z "> e. ( raG ` G ) ) )
34 eqidd 
 |-  ( z = v -> u = u )
35 eqidd 
 |-  ( z = v -> x = x )
36 id 
 |-  ( z = v -> z = v )
37 34 35 36 s3eqd 
 |-  ( z = v -> <" u x z "> = <" u x v "> )
38 37 eleq1d 
 |-  ( z = v -> ( <" u x z "> e. ( raG ` G ) <-> <" u x v "> e. ( raG ` G ) ) )
39 33 38 rspc2va 
 |-  ( ( ( u e. A /\ v e. B ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) -> <" u x v "> e. ( raG ` G ) )
40 26 27 28 39 syl21anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> <" u x v "> e. ( raG ` G ) )
41 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> x =/= u )
42 41 necomd 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> u =/= x )
43 42 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> u =/= x )
44 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> x =/= v )
45 44 necomd 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> v =/= x )
46 45 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> v =/= x )
47 1 2 3 4 25 10 24 17 21 40 43 46 ragncol 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> -. ( v e. ( u L x ) \/ u = x ) )
48 1 4 3 10 24 17 21 47 ncolrot2 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> -. ( x e. ( v L u ) \/ v = u ) )
49 1 3 4 10 17 21 24 17 48 tglineneq 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> ( x L v ) =/= ( u L x ) )
50 49 necomd 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> ( u L x ) =/= ( x L v ) )
51 1 3 4 11 23 16 42 42 12 22 15 tglinethru 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> A = ( u L x ) )
52 51 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> A = ( u L x ) )
53 13 elin2d 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> x e. B )
54 53 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> x e. B )
55 1 3 4 11 16 20 44 44 18 54 19 tglinethru 
 |-  ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> B = ( x L v ) )
56 55 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> B = ( x L v ) )
57 50 52 56 3netr4d 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) /\ v e. B ) /\ x =/= v ) -> A =/= B )
58 7 adantr 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> B e. ran L )
59 1 3 4 9 58 53 tglnpt2 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> E. v e. B x =/= v )
60 59 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) -> E. v e. B x =/= v )
61 57 60 r19.29a 
 |-  ( ( ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) /\ u e. A ) /\ x =/= u ) -> A =/= B )
62 6 adantr 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> A e. ran L )
63 1 3 4 9 62 14 tglnpt2 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> E. u e. A x =/= u )
64 63 adantr 
 |-  ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) -> E. u e. A x =/= u )
65 61 64 r19.29a 
 |-  ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) -> A =/= B )
66 1 2 3 4 5 6 7 isperp 
 |-  ( ph -> ( A ( perpG ` G ) B <-> E. x e. ( A i^i B ) A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) ) )
67 8 66 mpbid 
 |-  ( ph -> E. x e. ( A i^i B ) A. y e. A A. z e. B <" y x z "> e. ( raG ` G ) )
68 65 67 r19.29a 
 |-  ( ph -> A =/= B )