Metamath Proof Explorer

Theorem constrrtll

Description: In the construction of constructible numbers, line-line intersections are solutions of linear equations, and can therefore be completely constructed. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses constrrtll.s 
|- ( ph -> S C_ CC )
constrrtll.a 
|- ( ph -> A e. S )
constrrtll.b 
|- ( ph -> B e. S )
constrrtll.c 
|- ( ph -> C e. S )
constrrtll.d 
|- ( ph -> D e. S )
constrrtll.t 
|- ( ph -> T e. RR )
constrrtll.r 
|- ( ph -> R e. RR )
constrrtll.1 
|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
constrrtll.2 
|- ( ph -> X = ( C + ( R x. ( D - C ) ) ) )
constrrtll.3 
|- ( ph -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) =/= 0 )
constrrtll.n 
|- N = ( A + ( ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) x. ( B - A ) ) )
Assertion constrrtll 
|- ( ph -> X = N )

Proof

Step Hyp Ref Expression
1 constrrtll.s 
 |-  ( ph -> S C_ CC )
2 constrrtll.a 
 |-  ( ph -> A e. S )
3 constrrtll.b 
 |-  ( ph -> B e. S )
4 constrrtll.c 
 |-  ( ph -> C e. S )
5 constrrtll.d 
 |-  ( ph -> D e. S )
6 constrrtll.t 
 |-  ( ph -> T e. RR )
7 constrrtll.r 
 |-  ( ph -> R e. RR )
8 constrrtll.1 
 |-  ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
9 constrrtll.2 
 |-  ( ph -> X = ( C + ( R x. ( D - C ) ) ) )
10 constrrtll.3 
 |-  ( ph -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) =/= 0 )
11 constrrtll.n 
 |-  N = ( A + ( ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) x. ( B - A ) ) )
12 6 recnd 
 |-  ( ph -> T e. CC )
13 1 3 sseldd 
 |-  ( ph -> B e. CC )
14 1 2 sseldd 
 |-  ( ph -> A e. CC )
15 13 14 cjsubd 
 |-  ( ph -> ( * ` ( B - A ) ) = ( ( * ` B ) - ( * ` A ) ) )
16 13 14 subcld 
 |-  ( ph -> ( B - A ) e. CC )
17 16 cjcld 
 |-  ( ph -> ( * ` ( B - A ) ) e. CC )
18 15 17 eqeltrrd 
 |-  ( ph -> ( ( * ` B ) - ( * ` A ) ) e. CC )
19 1 5 sseldd 
 |-  ( ph -> D e. CC )
20 1 4 sseldd 
 |-  ( ph -> C e. CC )
21 19 20 subcld 
 |-  ( ph -> ( D - C ) e. CC )
22 18 21 mulcld 
 |-  ( ph -> ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) e. CC )
23 19 20 cjsubd 
 |-  ( ph -> ( * ` ( D - C ) ) = ( ( * ` D ) - ( * ` C ) ) )
24 21 cjcld 
 |-  ( ph -> ( * ` ( D - C ) ) e. CC )
25 23 24 eqeltrrd 
 |-  ( ph -> ( ( * ` D ) - ( * ` C ) ) e. CC )
26 16 25 mulcld 
 |-  ( ph -> ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) e. CC )
27 12 22 26 subdid 
 |-  ( ph -> ( T x. ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) = ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) - ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) )
28 8 oveq1d 
 |-  ( ph -> ( X - C ) = ( ( A + ( T x. ( B - A ) ) ) - C ) )
29 7 recnd 
 |-  ( ph -> R e. CC )
30 29 21 mulcld 
 |-  ( ph -> ( R x. ( D - C ) ) e. CC )
31 20 30 9 mvrladdd 
 |-  ( ph -> ( X - C ) = ( R x. ( D - C ) ) )
32 28 31 eqtr3d 
 |-  ( ph -> ( ( A + ( T x. ( B - A ) ) ) - C ) = ( R x. ( D - C ) ) )
33 32 30 eqeltrd 
 |-  ( ph -> ( ( A + ( T x. ( B - A ) ) ) - C ) e. CC )
34 fveq2 
 |-  ( ( ( * ` ( B - A ) ) x. ( D - C ) ) = 0 -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = ( Im ` 0 ) )
35 im0 
 |-  ( Im ` 0 ) = 0
36 34 35 eqtrdi 
 |-  ( ( ( * ` ( B - A ) ) x. ( D - C ) ) = 0 -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = 0 )
37 36 necon3i 
 |-  ( ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) =/= 0 -> ( ( * ` ( B - A ) ) x. ( D - C ) ) =/= 0 )
38 10 37 syl 
 |-  ( ph -> ( ( * ` ( B - A ) ) x. ( D - C ) ) =/= 0 )
39 17 21 38 mulne0bbd 
 |-  ( ph -> ( D - C ) =/= 0 )
40 33 29 21 39 divmul3d 
 |-  ( ph -> ( ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) = R <-> ( ( A + ( T x. ( B - A ) ) ) - C ) = ( R x. ( D - C ) ) ) )
41 32 40 mpbird 
 |-  ( ph -> ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) = R )
42 41 fveq2d 
 |-  ( ph -> ( * ` ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) ) = ( * ` R ) )
43 33 21 39 cjdivd 
 |-  ( ph -> ( * ` ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) ) = ( ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) / ( * ` ( D - C ) ) ) )
44 12 16 mulcld 
 |-  ( ph -> ( T x. ( B - A ) ) e. CC )
45 14 44 addcld 
 |-  ( ph -> ( A + ( T x. ( B - A ) ) ) e. CC )
46 45 20 cjsubd 
 |-  ( ph -> ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) = ( ( * ` ( A + ( T x. ( B - A ) ) ) ) - ( * ` C ) ) )
47 14 44 cjaddd 
 |-  ( ph -> ( * ` ( A + ( T x. ( B - A ) ) ) ) = ( ( * ` A ) + ( * ` ( T x. ( B - A ) ) ) ) )
48 12 16 cjmuld 
 |-  ( ph -> ( * ` ( T x. ( B - A ) ) ) = ( ( * ` T ) x. ( * ` ( B - A ) ) ) )
49 6 cjred 
 |-  ( ph -> ( * ` T ) = T )
50 49 15 oveq12d 
 |-  ( ph -> ( ( * ` T ) x. ( * ` ( B - A ) ) ) = ( T x. ( ( * ` B ) - ( * ` A ) ) ) )
51 48 50 eqtrd 
 |-  ( ph -> ( * ` ( T x. ( B - A ) ) ) = ( T x. ( ( * ` B ) - ( * ` A ) ) ) )
52 51 oveq2d 
 |-  ( ph -> ( ( * ` A ) + ( * ` ( T x. ( B - A ) ) ) ) = ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) )
53 47 52 eqtrd 
 |-  ( ph -> ( * ` ( A + ( T x. ( B - A ) ) ) ) = ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) )
54 53 oveq1d 
 |-  ( ph -> ( ( * ` ( A + ( T x. ( B - A ) ) ) ) - ( * ` C ) ) = ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) )
55 46 54 eqtrd 
 |-  ( ph -> ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) = ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) )
56 55 23 oveq12d 
 |-  ( ph -> ( ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) / ( * ` ( D - C ) ) ) = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) / ( ( * ` D ) - ( * ` C ) ) ) )
57 43 56 eqtrd 
 |-  ( ph -> ( * ` ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) ) = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) / ( ( * ` D ) - ( * ` C ) ) ) )
58 7 cjred 
 |-  ( ph -> ( * ` R ) = R )
59 42 57 58 3eqtr3rd 
 |-  ( ph -> R = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) / ( ( * ` D ) - ( * ` C ) ) ) )
60 41 59 eqtrd 
 |-  ( ph -> ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) / ( ( * ` D ) - ( * ` C ) ) ) )
61 14 cjcld 
 |-  ( ph -> ( * ` A ) e. CC )
62 12 18 mulcld 
 |-  ( ph -> ( T x. ( ( * ` B ) - ( * ` A ) ) ) e. CC )
63 61 62 addcld 
 |-  ( ph -> ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) e. CC )
64 20 cjcld 
 |-  ( ph -> ( * ` C ) e. CC )
65 63 64 subcld 
 |-  ( ph -> ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) e. CC )
66 21 39 cjne0d 
 |-  ( ph -> ( * ` ( D - C ) ) =/= 0 )
67 23 66 eqnetrrd 
 |-  ( ph -> ( ( * ` D ) - ( * ` C ) ) =/= 0 )
68 33 21 65 25 39 67 divmuleqd 
 |-  ( ph -> ( ( ( ( A + ( T x. ( B - A ) ) ) - C ) / ( D - C ) ) = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) / ( ( * ` D ) - ( * ` C ) ) ) <-> ( ( ( A + ( T x. ( B - A ) ) ) - C ) x. ( ( * ` D ) - ( * ` C ) ) ) = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) x. ( D - C ) ) ) )
69 60 68 mpbid 
 |-  ( ph -> ( ( ( A + ( T x. ( B - A ) ) ) - C ) x. ( ( * ` D ) - ( * ` C ) ) ) = ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) x. ( D - C ) ) )
70 14 44 20 addsubassd 
 |-  ( ph -> ( ( A + ( T x. ( B - A ) ) ) - C ) = ( A + ( ( T x. ( B - A ) ) - C ) ) )
71 44 14 20 addsub12d 
 |-  ( ph -> ( ( T x. ( B - A ) ) + ( A - C ) ) = ( A + ( ( T x. ( B - A ) ) - C ) ) )
72 70 71 eqtr4d 
 |-  ( ph -> ( ( A + ( T x. ( B - A ) ) ) - C ) = ( ( T x. ( B - A ) ) + ( A - C ) ) )
73 72 oveq1d 
 |-  ( ph -> ( ( ( A + ( T x. ( B - A ) ) ) - C ) x. ( ( * ` D ) - ( * ` C ) ) ) = ( ( ( T x. ( B - A ) ) + ( A - C ) ) x. ( ( * ` D ) - ( * ` C ) ) ) )
74 14 20 subcld 
 |-  ( ph -> ( A - C ) e. CC )
75 44 74 25 adddird 
 |-  ( ph -> ( ( ( T x. ( B - A ) ) + ( A - C ) ) x. ( ( * ` D ) - ( * ` C ) ) ) = ( ( ( T x. ( B - A ) ) x. ( ( * ` D ) - ( * ` C ) ) ) + ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) ) )
76 12 16 25 mulassd 
 |-  ( ph -> ( ( T x. ( B - A ) ) x. ( ( * ` D ) - ( * ` C ) ) ) = ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) )
77 76 oveq1d 
 |-  ( ph -> ( ( ( T x. ( B - A ) ) x. ( ( * ` D ) - ( * ` C ) ) ) + ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) ) = ( ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) + ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) ) )
78 73 75 77 3eqtrd 
 |-  ( ph -> ( ( ( A + ( T x. ( B - A ) ) ) - C ) x. ( ( * ` D ) - ( * ` C ) ) ) = ( ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) + ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) ) )
79 61 62 64 addsubassd 
 |-  ( ph -> ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) = ( ( * ` A ) + ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) - ( * ` C ) ) ) )
80 62 61 64 addsub12d 
 |-  ( ph -> ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) + ( ( * ` A ) - ( * ` C ) ) ) = ( ( * ` A ) + ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) - ( * ` C ) ) ) )
81 79 80 eqtr4d 
 |-  ( ph -> ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) = ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) + ( ( * ` A ) - ( * ` C ) ) ) )
82 81 oveq1d 
 |-  ( ph -> ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) x. ( D - C ) ) = ( ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) + ( ( * ` A ) - ( * ` C ) ) ) x. ( D - C ) ) )
83 61 64 subcld 
 |-  ( ph -> ( ( * ` A ) - ( * ` C ) ) e. CC )
84 62 83 21 adddird 
 |-  ( ph -> ( ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) + ( ( * ` A ) - ( * ` C ) ) ) x. ( D - C ) ) = ( ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) x. ( D - C ) ) + ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) )
85 12 18 21 mulassd 
 |-  ( ph -> ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) x. ( D - C ) ) = ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) )
86 85 oveq1d 
 |-  ( ph -> ( ( ( T x. ( ( * ` B ) - ( * ` A ) ) ) x. ( D - C ) ) + ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) = ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) + ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) )
87 82 84 86 3eqtrd 
 |-  ( ph -> ( ( ( ( * ` A ) + ( T x. ( ( * ` B ) - ( * ` A ) ) ) ) - ( * ` C ) ) x. ( D - C ) ) = ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) + ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) )
88 69 78 87 3eqtr3d 
 |-  ( ph -> ( ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) + ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) ) = ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) + ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) )
89 12 26 mulcld 
 |-  ( ph -> ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) e. CC )
90 74 25 mulcld 
 |-  ( ph -> ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) e. CC )
91 12 22 mulcld 
 |-  ( ph -> ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) e. CC )
92 83 21 mulcld 
 |-  ( ph -> ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) e. CC )
93 89 90 91 92 addsubeq4d 
 |-  ( ph -> ( ( ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) + ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) ) = ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) + ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) <-> ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) - ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) = ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) ) )
94 88 93 mpbid 
 |-  ( ph -> ( ( T x. ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) ) - ( T x. ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) = ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) )
95 27 94 eqtrd 
 |-  ( ph -> ( T x. ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) = ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) )
96 22 26 subcld 
 |-  ( ph -> ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) e. CC )
97 90 92 subcld 
 |-  ( ph -> ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) e. CC )
98 17 21 mulcld 
 |-  ( ph -> ( ( * ` ( B - A ) ) x. ( D - C ) ) e. CC )
99 reim0b 
 |-  ( ( ( * ` ( B - A ) ) x. ( D - C ) ) e. CC -> ( ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR <-> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = 0 ) )
100 98 99 syl 
 |-  ( ph -> ( ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR <-> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = 0 ) )
101 100 necon3bbid 
 |-  ( ph -> ( -. ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR <-> ( Im ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) =/= 0 ) )
102 10 101 mpbird 
 |-  ( ph -> -. ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR )
103 cjreb 
 |-  ( ( ( * ` ( B - A ) ) x. ( D - C ) ) e. CC -> ( ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR <-> ( * ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = ( ( * ` ( B - A ) ) x. ( D - C ) ) ) )
104 98 103 syl 
 |-  ( ph -> ( ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR <-> ( * ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = ( ( * ` ( B - A ) ) x. ( D - C ) ) ) )
105 104 necon3bbid 
 |-  ( ph -> ( -. ( ( * ` ( B - A ) ) x. ( D - C ) ) e. RR <-> ( * ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) =/= ( ( * ` ( B - A ) ) x. ( D - C ) ) ) )
106 102 105 mpbid 
 |-  ( ph -> ( * ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) =/= ( ( * ` ( B - A ) ) x. ( D - C ) ) )
107 17 21 cjmuld 
 |-  ( ph -> ( * ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = ( ( * ` ( * ` ( B - A ) ) ) x. ( * ` ( D - C ) ) ) )
108 16 cjcjd 
 |-  ( ph -> ( * ` ( * ` ( B - A ) ) ) = ( B - A ) )
109 108 23 oveq12d 
 |-  ( ph -> ( ( * ` ( * ` ( B - A ) ) ) x. ( * ` ( D - C ) ) ) = ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) )
110 107 109 eqtrd 
 |-  ( ph -> ( * ` ( ( * ` ( B - A ) ) x. ( D - C ) ) ) = ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) )
111 15 oveq1d 
 |-  ( ph -> ( ( * ` ( B - A ) ) x. ( D - C ) ) = ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) )
112 106 110 111 3netr3d 
 |-  ( ph -> ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) =/= ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) )
113 112 necomd 
 |-  ( ph -> ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) =/= ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) )
114 22 26 113 subne0d 
 |-  ( ph -> ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) =/= 0 )
115 12 96 97 114 ldiv 
 |-  ( ph -> ( ( T x. ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) = ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) <-> T = ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) ) )
116 95 115 mpbid 
 |-  ( ph -> T = ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) )
117 116 oveq1d 
 |-  ( ph -> ( T x. ( B - A ) ) = ( ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) x. ( B - A ) ) )
118 117 oveq2d 
 |-  ( ph -> ( A + ( T x. ( B - A ) ) ) = ( A + ( ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) x. ( B - A ) ) ) )
119 8 118 eqtrd 
 |-  ( ph -> X = ( A + ( ( ( ( ( A - C ) x. ( ( * ` D ) - ( * ` C ) ) ) - ( ( ( * ` A ) - ( * ` C ) ) x. ( D - C ) ) ) / ( ( ( ( * ` B ) - ( * ` A ) ) x. ( D - C ) ) - ( ( B - A ) x. ( ( * ` D ) - ( * ` C ) ) ) ) ) x. ( B - A ) ) ) )
120 119 11 eqtr4di 
 |-  ( ph -> X = N )