Metamath Proof Explorer

Theorem perpprlng

Description: If two lines A and B have a common perpendicular C and lie in the same plane H , then they are parallel. Theorem 12.9 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses perpprlng.p 
|- P = ( Base ` G )
perpprlng.l 
|- L = ( LineG ` G )
perpprlng.e 
|- E = ( PlnG ` G )
perpprlng.r 
|- .|| = ( parlnG ` G )
perpprlng.g 
|- ( ph -> G e. TarskiG )
perpprlng.h 
|- ( ph -> H e. ran E )
perpprlng.a 
|- ( ph -> A C_ H )
perpprlng.b 
|- ( ph -> B C_ H )
perpprlng.1 
|- ( ph -> C C_ H )
perpprlng.q 
|- ( ph -> A ( perpG ` G ) C )
perpprlng.2 
|- ( ph -> B ( perpG ` G ) C )
Assertion perpprlng 
|- ( ph -> A .|| B )

Proof

Step Hyp Ref Expression
1 perpprlng.p 
 |-  P = ( Base ` G )
2 perpprlng.l 
 |-  L = ( LineG ` G )
3 perpprlng.e 
 |-  E = ( PlnG ` G )
4 perpprlng.r 
 |-  .|| = ( parlnG ` G )
5 perpprlng.g 
 |-  ( ph -> G e. TarskiG )
6 perpprlng.h 
 |-  ( ph -> H e. ran E )
7 perpprlng.a 
 |-  ( ph -> A C_ H )
8 perpprlng.b 
 |-  ( ph -> B C_ H )
9 perpprlng.1 
 |-  ( ph -> C C_ H )
10 perpprlng.q 
 |-  ( ph -> A ( perpG ` G ) C )
11 perpprlng.2 
 |-  ( ph -> B ( perpG ` G ) C )
12 5 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> G e. TarskiG )
13 2 5 10 perpln1 
 |-  ( ph -> A e. ran L )
14 13 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> A e. ran L )
15 2 5 11 perpln1 
 |-  ( ph -> B e. ran L )
16 15 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> B e. ran L )
17 6 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> H e. ran E )
18 7 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> A C_ H )
19 8 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> B C_ H )
20 simpr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> ( A i^i B ) = (/) )
21 2 3 4 12 14 16 17 18 19 20 prlngd 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> A .|| B )
22 5 adantr 
 |-  ( ( ph /\ ( A i^i B ) =/= (/) ) -> G e. TarskiG )
23 13 adantr 
 |-  ( ( ph /\ ( A i^i B ) =/= (/) ) -> A e. ran L )
24 2 3 4 22 23 prlngref 
 |-  ( ( ph /\ ( A i^i B ) =/= (/) ) -> A .|| A )
25 simpr 
 |-  ( ( ph /\ ( A i^i B ) =/= (/) ) -> ( A i^i B ) =/= (/) )
26 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> G e. TarskiG )
27 2 5 10 perpln2 
 |-  ( ph -> C e. ran L )
28 27 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> C e. ran L )
29 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> H e. ran E )
30 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> x e. C )
31 9 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> C C_ H )
32 7 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> A C_ H )
33 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> z e. ( A \ C ) )
34 33 eldifad 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> z e. A )
35 32 34 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> z e. H )
36 8 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> B C_ H )
37 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> y e. ( B \ C ) )
38 37 eldifad 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> y e. B )
39 36 38 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> y e. H )
40 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
41 13 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> A e. ran L )
42 simpr 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> x e. ( A i^i B ) )
43 42 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> x e. ( A i^i B ) )
44 43 elin1d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> x e. A )
45 1 2 40 26 41 44 tglnpt 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> x e. P )
46 1 2 40 26 41 34 tglnpt 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> z e. P )
47 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> z =/= x )
48 47 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> x =/= z )
49 1 40 2 26 45 46 48 48 41 44 34 tglinethru 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> A = ( x L z ) )
50 10 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> A ( perpG ` G ) C )
51 49 50 eqbrtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> ( x L z ) ( perpG ` G ) C )
52 22 adantr 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> G e. TarskiG )
53 52 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> G e. TarskiG )
54 15 ad2antrr 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> B e. ran L )
55 54 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> B e. ran L )
56 42 elin2d 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> x e. B )
57 56 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> x e. B )
58 1 2 40 53 55 57 tglnpt 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> x e. P )
59 simplr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> y e. ( B \ C ) )
60 59 eldifad 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> y e. B )
61 1 2 40 53 55 60 tglnpt 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> y e. P )
62 simpr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> y =/= x )
63 62 necomd 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> x =/= y )
64 1 40 2 53 58 61 63 63 55 57 60 tglinethru 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> B = ( x L y ) )
65 64 adantllr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> B = ( x L y ) )
66 65 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> B = ( x L y ) )
67 11 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> B ( perpG ` G ) C )
68 66 67 eqbrtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> ( x L y ) ( perpG ` G ) C )
69 1 2 3 26 28 29 30 31 35 39 51 68 perpeq 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> ( x L z ) = ( x L y ) )
70 69 49 66 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) /\ z e. ( A \ C ) ) /\ z =/= x ) -> A = B )
71 23 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> A e. ran L )
72 27 ad2antrr 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> C e. ran L )
73 72 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> C e. ran L )
74 simpllr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> x e. ( A i^i B ) )
75 74 elin1d 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> x e. A )
76 eqid 
 |-  ( dist ` G ) = ( dist ` G )
77 1 76 40 2 5 13 27 10 perpneq 
 |-  ( ph -> A =/= C )
78 77 ad4antr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> A =/= C )
79 1 40 2 53 71 73 75 78 tglnpt4 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> E. z e. ( A \ C ) z =/= x )
80 79 adantllr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> E. z e. ( A \ C ) z =/= x )
81 70 80 r19.29a 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) /\ y e. ( B \ C ) ) /\ y =/= x ) -> A = B )
82 1 76 40 2 5 15 27 11 perpneq 
 |-  ( ph -> B =/= C )
83 82 ad2antrr 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> B =/= C )
84 1 40 2 52 54 72 56 83 tglnpt4 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> E. y e. ( B \ C ) y =/= x )
85 84 adantr 
 |-  ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) -> E. y e. ( B \ C ) y =/= x )
86 81 85 r19.29a 
 |-  ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ x e. C ) -> A = B )
87 52 adantr 
 |-  ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) -> G e. TarskiG )
88 10 ad3antrrr 
 |-  ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) -> A ( perpG ` G ) C )
89 87 88 perpin 
 |-  ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) -> ( A i^i C ) =/= (/) )
90 87 adantr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) -> G e. TarskiG )
91 11 ad2antrr 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> B ( perpG ` G ) C )
92 91 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) -> B ( perpG ` G ) C )
93 90 92 perpin 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) -> ( B i^i C ) =/= (/) )
94 90 adantr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> G e. TarskiG )
95 72 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> C e. ran L )
96 simplr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> y e. ( A i^i C ) )
97 96 elin2d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> y e. C )
98 simpr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> z e. ( B i^i C ) )
99 98 elin2d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> z e. C )
100 23 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> A e. ran L )
101 simp-4r 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> x e. ( A i^i B ) )
102 101 elin1d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> x e. A )
103 1 2 40 94 100 102 tglnpt 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> x e. P )
104 1 2 40 94 95 97 tglnpt 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> y e. P )
105 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> -. x e. C )
106 nelne2 
 |-  ( ( y e. C /\ -. x e. C ) -> y =/= x )
107 97 105 106 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> y =/= x )
108 96 elin1d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> y e. A )
109 1 40 2 94 104 103 107 107 100 108 102 tglinethru 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> A = ( y L x ) )
110 88 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> A ( perpG ` G ) C )
111 109 110 eqbrtrrd 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> ( y L x ) ( perpG ` G ) C )
112 1 2 40 94 95 99 tglnpt 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> z e. P )
113 nelne2 
 |-  ( ( z e. C /\ -. x e. C ) -> z =/= x )
114 99 105 113 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> z =/= x )
115 54 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> B e. ran L )
116 98 elin1d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> z e. B )
117 56 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> x e. B )
118 1 40 2 94 112 103 114 114 115 116 117 tglinethru 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> B = ( z L x ) )
119 92 adantr 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> B ( perpG ` G ) C )
120 118 119 eqbrtrrd 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> ( z L x ) ( perpG ` G ) C )
121 1 76 40 2 94 95 97 99 103 111 120 footeq 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> y = z )
122 121 oveq2d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> ( x L y ) = ( x L z ) )
123 107 necomd 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> x =/= y )
124 1 40 2 94 103 104 123 123 100 102 108 tglinethru 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> A = ( x L y ) )
125 114 necomd 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> x =/= z )
126 1 40 2 94 103 112 125 125 115 117 116 tglinethru 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> B = ( x L z ) )
127 122 124 126 3eqtr4d 
 |-  ( ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) /\ z e. ( B i^i C ) ) -> A = B )
128 93 127 n0limd 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) /\ y e. ( A i^i C ) ) -> A = B )
129 89 128 n0limd 
 |-  ( ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) /\ -. x e. C ) -> A = B )
130 86 129 pm2.61dan 
 |-  ( ( ( ph /\ ( A i^i B ) =/= (/) ) /\ x e. ( A i^i B ) ) -> A = B )
131 25 130 n0limd 
 |-  ( ( ph /\ ( A i^i B ) =/= (/) ) -> A = B )
132 24 131 breqtrd 
 |-  ( ( ph /\ ( A i^i B ) =/= (/) ) -> A .|| B )
133 21 132 pm2.61dane 
 |-  ( ph -> A .|| B )