Metamath Proof Explorer

Theorem crossp3d

Description: The vector triple product expansion (BAC-CAB rule): the cross product of X with ( Y crossp Z ) equals Y scaled by the dot product of X and Z , minus Z scaled by the dot product of X and Y . The dot products are written out as explicit three-term sums of component products, matching the pointwise style of df-crossp rather than introducing a separate dot product operator. (Contributed by Jiamin Zhao, 12-Aug-2026)

Ref Expression
Hypotheses crossp3d.1 
|- ( ph -> X e. ( RR ^m ( 1 ... 3 ) ) )
crossp3d.2 
|- ( ph -> Y e. ( RR ^m ( 1 ... 3 ) ) )
crossp3d.3 
|- ( ph -> Z e. ( RR ^m ( 1 ... 3 ) ) )
Assertion crossp3d 
|- ( ph -> ( X crossp ( Y crossp Z ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 crossp3d.1 
 |-  ( ph -> X e. ( RR ^m ( 1 ... 3 ) ) )
2 crossp3d.2 
 |-  ( ph -> Y e. ( RR ^m ( 1 ... 3 ) ) )
3 crossp3d.3 
 |-  ( ph -> Z e. ( RR ^m ( 1 ... 3 ) ) )
4 2 3 crosspcld 
 |-  ( ph -> ( Y crossp Z ) e. ( RR ^m ( 1 ... 3 ) ) )
5 1 4 crosspcld 
 |-  ( ph -> ( X crossp ( Y crossp Z ) ) e. ( RR ^m ( 1 ... 3 ) ) )
6 elmapi 
 |-  ( ( X crossp ( Y crossp Z ) ) e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR )
7 5 6 syl 
 |-  ( ph -> ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR )
8 7 ffnd 
 |-  ( ph -> ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) )
9 ovex 
 |-  ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) e. _V
10 eqid 
 |-  ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) )
11 9 10 fnmpti 
 |-  ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) Fn ( 1 ... 3 )
12 11 a1i 
 |-  ( ph -> ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) Fn ( 1 ... 3 ) )
13 simpr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> t = 1 )
14 13 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` 1 ) )
15 1 4 crosspv1d 
 |-  ( ph -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) )
16 15 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) )
17 2 3 crosspv3d 
 |-  ( ph -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) )
18 17 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) )
19 18 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) = ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) )
20 2 3 crosspv2d 
 |-  ( ph -> ( ( Y crossp Z ) ` 2 ) = ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) )
21 20 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y crossp Z ) ` 2 ) = ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) )
22 21 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) = ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) )
23 19 22 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) )
24 16 23 eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) )
25 1 rr3fv2cld 
 |-  ( ph -> ( X ` 2 ) e. RR )
26 25 recnd 
 |-  ( ph -> ( X ` 2 ) e. CC )
27 26 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( X ` 2 ) e. CC )
28 2 rr3fv1cld 
 |-  ( ph -> ( Y ` 1 ) e. RR )
29 3 rr3fv2cld 
 |-  ( ph -> ( Z ` 2 ) e. RR )
30 28 29 remulcld 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 2 ) ) e. RR )
31 30 recnd 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 2 ) ) e. CC )
32 31 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y ` 1 ) x. ( Z ` 2 ) ) e. CC )
33 2 rr3fv2cld 
 |-  ( ph -> ( Y ` 2 ) e. RR )
34 3 rr3fv1cld 
 |-  ( ph -> ( Z ` 1 ) e. RR )
35 33 34 remulcld 
 |-  ( ph -> ( ( Y ` 2 ) x. ( Z ` 1 ) ) e. RR )
36 35 recnd 
 |-  ( ph -> ( ( Y ` 2 ) x. ( Z ` 1 ) ) e. CC )
37 36 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y ` 2 ) x. ( Z ` 1 ) ) e. CC )
38 27 32 37 subdid 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) )
39 1 rr3fv3cld 
 |-  ( ph -> ( X ` 3 ) e. RR )
40 39 recnd 
 |-  ( ph -> ( X ` 3 ) e. CC )
41 40 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( X ` 3 ) e. CC )
42 2 rr3fv3cld 
 |-  ( ph -> ( Y ` 3 ) e. RR )
43 42 34 remulcld 
 |-  ( ph -> ( ( Y ` 3 ) x. ( Z ` 1 ) ) e. RR )
44 43 recnd 
 |-  ( ph -> ( ( Y ` 3 ) x. ( Z ` 1 ) ) e. CC )
45 44 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y ` 3 ) x. ( Z ` 1 ) ) e. CC )
46 3 rr3fv3cld 
 |-  ( ph -> ( Z ` 3 ) e. RR )
47 28 46 remulcld 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 3 ) ) e. RR )
48 47 recnd 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 3 ) ) e. CC )
49 48 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y ` 1 ) x. ( Z ` 3 ) ) e. CC )
50 41 45 49 subdid 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) = ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) )
51 38 50 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) )
52 1 rr3fv1cld 
 |-  ( ph -> ( X ` 1 ) e. RR )
53 52 recnd 
 |-  ( ph -> ( X ` 1 ) e. CC )
54 34 recnd 
 |-  ( ph -> ( Z ` 1 ) e. CC )
55 53 54 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( Z ` 1 ) ) e. CC )
56 29 recnd 
 |-  ( ph -> ( Z ` 2 ) e. CC )
57 26 56 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( Z ` 2 ) ) e. CC )
58 55 57 addcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) e. CC )
59 58 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) e. CC )
60 46 recnd 
 |-  ( ph -> ( Z ` 3 ) e. CC )
61 40 60 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( Z ` 3 ) ) e. CC )
62 61 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( Z ` 3 ) ) e. CC )
63 28 recnd 
 |-  ( ph -> ( Y ` 1 ) e. CC )
64 63 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Y ` 1 ) e. CC )
65 59 62 64 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) ) )
66 53 63 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( Y ` 1 ) ) e. CC )
67 33 recnd 
 |-  ( ph -> ( Y ` 2 ) e. CC )
68 26 67 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( Y ` 2 ) ) e. CC )
69 66 68 addcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) e. CC )
70 69 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) e. CC )
71 42 recnd 
 |-  ( ph -> ( Y ` 3 ) e. CC )
72 40 71 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( Y ` 3 ) ) e. CC )
73 72 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( Y ` 3 ) ) e. CC )
74 54 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Z ` 1 ) e. CC )
75 70 73 74 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) )
76 65 75 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) )
77 58 63 mulcld 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) e. CC )
78 77 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) e. CC )
79 61 63 mulcld 
 |-  ( ph -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) e. CC )
80 79 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) e. CC )
81 69 54 mulcld 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) e. CC )
82 81 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) e. CC )
83 72 54 mulcld 
 |-  ( ph -> ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) e. CC )
84 83 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) e. CC )
85 78 80 82 84 addsub4d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) )
86 55 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 1 ) x. ( Z ` 1 ) ) e. CC )
87 57 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( Z ` 2 ) ) e. CC )
88 86 87 64 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) = ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) )
89 66 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 1 ) x. ( Y ` 1 ) ) e. CC )
90 68 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( Y ` 2 ) ) e. CC )
91 89 90 74 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) = ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) )
92 88 91 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) )
93 92 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) )
94 53 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( X ` 1 ) e. CC )
95 94 74 64 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) = ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 1 ) ) ) )
96 74 64 mulcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Z ` 1 ) x. ( Y ` 1 ) ) = ( ( Y ` 1 ) x. ( Z ` 1 ) ) )
97 96 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 1 ) ) ) = ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) )
98 95 97 eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) = ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) )
99 98 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) )
100 99 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) )
101 100 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) )
102 94 64 74 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) = ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) )
103 102 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) )
104 103 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) )
105 104 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) )
106 56 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Z ` 2 ) e. CC )
107 27 106 64 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) = ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 1 ) ) ) )
108 106 64 mulcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Z ` 2 ) x. ( Y ` 1 ) ) = ( ( Y ` 1 ) x. ( Z ` 2 ) ) )
109 108 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 1 ) ) ) = ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) )
110 107 109 eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) = ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) )
111 67 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Y ` 2 ) e. CC )
112 27 111 74 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) = ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) )
113 110 112 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) )
114 60 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Z ` 3 ) e. CC )
115 41 114 64 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) = ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 1 ) ) ) )
116 114 64 mulcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Z ` 3 ) x. ( Y ` 1 ) ) = ( ( Y ` 1 ) x. ( Z ` 3 ) ) )
117 116 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 1 ) ) ) = ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) )
118 115 117 eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) = ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) )
119 71 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Y ` 3 ) e. CC )
120 41 119 74 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) = ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) )
121 118 120 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) = ( ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) ) )
122 113 121 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) ) ) )
123 63 54 mulcld 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 1 ) ) e. CC )
124 53 123 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) e. CC )
125 124 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) e. CC )
126 57 63 mulcld 
 |-  ( ph -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) e. CC )
127 126 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) e. CC )
128 68 54 mulcld 
 |-  ( ph -> ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) e. CC )
129 128 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) e. CC )
130 125 127 129 pnpcand 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) )
131 130 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) )
132 63 56 mulcld 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 2 ) ) e. CC )
133 26 132 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) e. CC )
134 67 54 mulcld 
 |-  ( ph -> ( ( Y ` 2 ) x. ( Z ` 1 ) ) e. CC )
135 26 134 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) e. CC )
136 133 135 subcld 
 |-  ( ph -> ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) e. CC )
137 136 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) e. CC )
138 71 54 mulcld 
 |-  ( ph -> ( ( Y ` 3 ) x. ( Z ` 1 ) ) e. CC )
139 40 138 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) e. CC )
140 139 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) e. CC )
141 63 60 mulcld 
 |-  ( ph -> ( ( Y ` 1 ) x. ( Z ` 3 ) ) e. CC )
142 40 141 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) e. CC )
143 142 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) e. CC )
144 137 140 143 subsub2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) ) ) )
145 122 131 144 3eqtr4d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 1 ) ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) )
146 101 105 145 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 1 ) ) ) ) + ( ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) - ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) )
147 85 93 146 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 1 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 1 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 1 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 1 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) )
148 76 147 eqtr2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( X ` 2 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) ) )
149 24 51 148 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) ) )
150 13 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> 1 = t )
151 150 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Y ` 1 ) = ( Y ` t ) )
152 151 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) )
153 150 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( Z ` 1 ) = ( Z ` t ) )
154 153 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) )
155 152 154 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
156 14 149 155 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
157 simpr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> t = ( 1 + 1 ) )
158 1p1e2 
 |-  ( 1 + 1 ) = 2
159 157 158 eqtrdi 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> t = 2 )
160 159 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` 2 ) )
161 1 4 crosspv2d 
 |-  ( ph -> ( ( X crossp ( Y crossp Z ) ) ` 2 ) = ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) )
162 161 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 2 ) = ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) )
163 2 3 crosspv1d 
 |-  ( ph -> ( ( Y crossp Z ) ` 1 ) = ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) )
164 163 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y crossp Z ) ` 1 ) = ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) )
165 164 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) = ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
166 17 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) )
167 166 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) = ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) )
168 165 167 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) )
169 40 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( X ` 3 ) e. CC )
170 67 60 mulcld 
 |-  ( ph -> ( ( Y ` 2 ) x. ( Z ` 3 ) ) e. CC )
171 170 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y ` 2 ) x. ( Z ` 3 ) ) e. CC )
172 71 56 mulcld 
 |-  ( ph -> ( ( Y ` 3 ) x. ( Z ` 2 ) ) e. CC )
173 172 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y ` 3 ) x. ( Z ` 2 ) ) e. CC )
174 169 171 173 subdid 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
175 53 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( X ` 1 ) e. CC )
176 132 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y ` 1 ) x. ( Z ` 2 ) ) e. CC )
177 134 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y ` 2 ) x. ( Z ` 1 ) ) e. CC )
178 175 176 177 subdid 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) )
179 174 178 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) = ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) )
180 53 134 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) e. CC )
181 180 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) e. CC )
182 67 56 mulcld 
 |-  ( ph -> ( ( Y ` 2 ) x. ( Z ` 2 ) ) e. CC )
183 26 182 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) e. CC )
184 183 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) e. CC )
185 181 184 addcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) )
186 185 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) )
187 53 132 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) e. CC )
188 187 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) e. CC )
189 188 184 addcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) )
190 189 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
191 186 190 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
192 40 170 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) e. CC )
193 192 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) e. CC )
194 184 181 193 addassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) ) )
195 40 172 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) e. CC )
196 195 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) e. CC )
197 184 188 196 addassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
198 194 197 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) ) )
199 180 192 addcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) e. CC )
200 199 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) e. CC )
201 187 195 addcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) e. CC )
202 201 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) e. CC )
203 184 200 202 pnpcand 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
204 193 196 188 181 subadd4d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) = ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) ) )
205 193 181 addcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) )
206 196 188 addcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
207 205 206 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
208 204 207 eqtr2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) )
209 198 203 208 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) )
210 191 209 eqtr2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
211 54 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Z ` 1 ) e. CC )
212 67 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Y ` 2 ) e. CC )
213 211 212 mulcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Z ` 1 ) x. ( Y ` 2 ) ) = ( ( Y ` 2 ) x. ( Z ` 1 ) ) )
214 213 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) = ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) )
215 214 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) = ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) )
216 56 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Z ` 2 ) e. CC )
217 216 212 mulcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Z ` 2 ) x. ( Y ` 2 ) ) = ( ( Y ` 2 ) x. ( Z ` 2 ) ) )
218 217 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) = ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) )
219 218 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) = ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) )
220 215 219 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) ) )
221 220 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) )
222 221 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
223 175 211 212 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) = ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) )
224 223 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) )
225 26 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( X ` 2 ) e. CC )
226 225 216 212 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) = ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) )
227 226 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) )
228 224 227 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) )
229 228 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) )
230 63 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Y ` 1 ) e. CC )
231 175 230 216 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) = ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) )
232 231 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) = ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) )
233 225 212 216 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) = ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) )
234 233 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) )
235 232 234 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) )
236 235 oveq1d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
237 229 236 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
238 210 222 237 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
239 55 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( Z ` 1 ) ) e. CC )
240 57 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( Z ` 2 ) ) e. CC )
241 239 240 212 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) = ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) )
242 241 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) = ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) )
243 40 60 67 mulassd 
 |-  ( ph -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) = ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 2 ) ) ) )
244 60 67 mulcomd 
 |-  ( ph -> ( ( Z ` 3 ) x. ( Y ` 2 ) ) = ( ( Y ` 2 ) x. ( Z ` 3 ) ) )
245 244 oveq2d 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 2 ) ) ) = ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) )
246 243 245 eqtr2d 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) = ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) )
247 246 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) = ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) )
248 242 247 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) ) )
249 66 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( Y ` 1 ) ) e. CC )
250 68 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 2 ) x. ( Y ` 2 ) ) e. CC )
251 249 250 216 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) = ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) )
252 71 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Y ` 3 ) e. CC )
253 169 252 216 mulassd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) = ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) )
254 251 253 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
255 254 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) ) )
256 248 255 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) ) ) )
257 58 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) e. CC )
258 61 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( Z ` 3 ) ) e. CC )
259 257 258 212 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) ) )
260 259 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) )
261 69 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) e. CC )
262 72 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( Y ` 3 ) ) e. CC )
263 261 262 216 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) ) )
264 263 eqcomd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) )
265 260 264 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 2 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 2 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 2 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 2 ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) ) )
266 238 256 265 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( X ` 3 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 2 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) ) )
267 168 179 266 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) ) )
268 159 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Y ` t ) = ( Y ` 2 ) )
269 268 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) )
270 159 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( Z ` t ) = ( Z ` 2 ) )
271 270 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) )
272 269 271 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) ) )
273 267 272 eqtr4d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
274 160 162 273 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
275 simpr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> t = ( 1 + 2 ) )
276 275 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` ( 1 + 2 ) ) )
277 1p2e3 
 |-  ( 1 + 2 ) = 3
278 277 a1i 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( 1 + 2 ) = 3 )
279 278 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` ( 1 + 2 ) ) = ( ( X crossp ( Y crossp Z ) ) ` 3 ) )
280 1 4 crosspv3d 
 |-  ( ph -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) )
281 280 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) )
282 20 oveq2d 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) = ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) )
283 163 oveq2d 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) = ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
284 282 283 oveq12d 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
285 284 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
286 275 277 eqtrdi 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> t = 3 )
287 286 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( Y ` t ) = ( Y ` 3 ) )
288 287 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` t ) ) = ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) )
289 287 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` t ) ) = ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) )
290 288 289 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` t ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` t ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) ) )
291 286 fveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( Z ` t ) = ( Z ` 3 ) )
292 291 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` t ) ) = ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) )
293 291 oveq2d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` t ) ) = ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) )
294 292 293 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` t ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` t ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) ) )
295 290 294 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` t ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` t ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` t ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` t ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) ) ) )
296 55 57 71 adddird 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) = ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) ) )
297 40 60 71 mulassd 
 |-  ( ph -> ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) = ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) )
298 296 297 oveq12d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) )
299 66 68 60 adddird 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) = ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) ) )
300 40 71 60 mulassd 
 |-  ( ph -> ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) = ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 3 ) ) ) )
301 299 300 oveq12d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 3 ) ) ) ) )
302 298 301 oveq12d 
 |-  ( ph -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 3 ) ) ) ) ) )
303 53 54 71 mulassd 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) = ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) )
304 26 56 71 mulassd 
 |-  ( ph -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) = ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 3 ) ) ) )
305 56 71 mulcomd 
 |-  ( ph -> ( ( Z ` 2 ) x. ( Y ` 3 ) ) = ( ( Y ` 3 ) x. ( Z ` 2 ) ) )
306 305 oveq2d 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Z ` 2 ) x. ( Y ` 3 ) ) ) = ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) )
307 304 306 eqtrd 
 |-  ( ph -> ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) = ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) )
308 303 307 oveq12d 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) ) = ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
309 308 oveq1d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) )
310 53 63 60 mulassd 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) = ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) )
311 26 67 60 mulassd 
 |-  ( ph -> ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) = ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) )
312 310 311 oveq12d 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) )
313 71 60 mulcomd 
 |-  ( ph -> ( ( Y ` 3 ) x. ( Z ` 3 ) ) = ( ( Z ` 3 ) x. ( Y ` 3 ) ) )
314 313 oveq2d 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 3 ) ) ) = ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) )
315 312 314 oveq12d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) )
316 309 315 oveq12d 
 |-  ( ph -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 2 ) x. ( Z ` 2 ) ) x. ( Y ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 2 ) x. ( Y ` 2 ) ) x. ( Z ` 3 ) ) ) + ( ( X ` 3 ) x. ( ( Y ` 3 ) x. ( Z ` 3 ) ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) ) )
317 53 138 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) e. CC )
318 26 172 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) e. CC )
319 317 318 addcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) e. CC )
320 53 141 mulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) e. CC )
321 26 170 mulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) e. CC )
322 320 321 addcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) e. CC )
323 60 71 mulcld 
 |-  ( ph -> ( ( Z ` 3 ) x. ( Y ` 3 ) ) e. CC )
324 40 323 mulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) e. CC )
325 319 322 324 pnpcan2d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) ) )
326 54 71 mulcomd 
 |-  ( ph -> ( ( Z ` 1 ) x. ( Y ` 3 ) ) = ( ( Y ` 3 ) x. ( Z ` 1 ) ) )
327 326 oveq2d 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) = ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) )
328 327 oveq1d 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
329 328 oveq1d 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) )
330 329 oveq1d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) ) = ( ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) ) )
331 317 320 321 318 subadd4d 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) ) )
332 325 330 331 3eqtr4d 
 |-  ( ph -> ( ( ( ( ( X ` 1 ) x. ( ( Z ` 1 ) x. ( Y ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) - ( ( ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) + ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) ) + ( ( X ` 3 ) x. ( ( Z ` 3 ) x. ( Y ` 3 ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
333 302 316 332 3eqtrd 
 |-  ( ph -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
334 333 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` 3 ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` 3 ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` 3 ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` 3 ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
335 295 334 eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` t ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` t ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` t ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` t ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
336 58 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) e. CC )
337 61 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X ` 3 ) x. ( Z ` 3 ) ) e. CC )
338 elmapi 
 |-  ( Y e. ( RR ^m ( 1 ... 3 ) ) -> Y : ( 1 ... 3 ) --> RR )
339 2 338 syl 
 |-  ( ph -> Y : ( 1 ... 3 ) --> RR )
340 339 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> Y : ( 1 ... 3 ) --> RR )
341 simplr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> t e. ( 1 ... 3 ) )
342 340 341 ffvelcdmd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( Y ` t ) e. RR )
343 342 recnd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( Y ` t ) e. CC )
344 336 337 343 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` t ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` t ) ) ) )
345 69 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) e. CC )
346 72 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X ` 3 ) x. ( Y ` 3 ) ) e. CC )
347 elmapi 
 |-  ( Z e. ( RR ^m ( 1 ... 3 ) ) -> Z : ( 1 ... 3 ) --> RR )
348 3 347 syl 
 |-  ( ph -> Z : ( 1 ... 3 ) --> RR )
349 348 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> Z : ( 1 ... 3 ) --> RR )
350 349 341 ffvelcdmd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( Z ` t ) e. RR )
351 350 recnd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( Z ` t ) e. CC )
352 345 346 351 adddird 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` t ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` t ) ) ) )
353 344 352 oveq12d 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) x. ( Y ` t ) ) + ( ( ( X ` 3 ) x. ( Z ` 3 ) ) x. ( Y ` t ) ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) x. ( Z ` t ) ) + ( ( ( X ` 3 ) x. ( Y ` 3 ) ) x. ( Z ` t ) ) ) ) )
354 53 138 141 subdid 
 |-  ( ph -> ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) = ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) )
355 26 170 172 subdid 
 |-  ( ph -> ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) = ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) )
356 354 355 oveq12d 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
357 356 ad2antrr 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( X ` 1 ) x. ( ( Y ` 3 ) x. ( Z ` 1 ) ) ) - ( ( X ` 1 ) x. ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( ( X ` 2 ) x. ( ( Y ` 2 ) x. ( Z ` 3 ) ) ) - ( ( X ` 2 ) x. ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) )
358 335 353 357 3eqtr4rd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
359 281 285 358 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
360 276 279 359 3eqtrd 
 |-  ( ( ( ph /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
361 simpr 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> t e. ( 1 ... 3 ) )
362 277 eqcomi 
 |-  3 = ( 1 + 2 )
363 362 oveq2i 
 |-  ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
364 1z 
 |-  1 e. ZZ
365 fztp 
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
366 364 365 ax-mp 
 |-  ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
367 363 366 eqtri 
 |-  ( 1 ... 3 ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
368 361 367 eleqtrdi 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> t e. { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
369 eltpi 
 |-  ( t e. { 1 , ( 1 + 1 ) , ( 1 + 2 ) } -> ( t = 1 \/ t = ( 1 + 1 ) \/ t = ( 1 + 2 ) ) )
370 368 369 syl 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( t = 1 \/ t = ( 1 + 1 ) \/ t = ( 1 + 2 ) ) )
371 156 274 360 370 mpjao3dan 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
372 fveq2 
 |-  ( k = t -> ( Y ` k ) = ( Y ` t ) )
373 372 oveq2d 
 |-  ( k = t -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) = ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) )
374 fveq2 
 |-  ( k = t -> ( Z ` k ) = ( Z ` t ) )
375 374 oveq2d 
 |-  ( k = t -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) = ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) )
376 373 375 oveq12d 
 |-  ( k = t -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
377 52 34 remulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( Z ` 1 ) ) e. RR )
378 25 29 remulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( Z ` 2 ) ) e. RR )
379 377 378 readdcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) e. RR )
380 39 46 remulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( Z ` 3 ) ) e. RR )
381 379 380 readdcld 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) e. RR )
382 381 adantr 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) e. RR )
383 339 ffvelcdmda 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( Y ` t ) e. RR )
384 382 383 remulcld 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) e. RR )
385 52 28 remulcld 
 |-  ( ph -> ( ( X ` 1 ) x. ( Y ` 1 ) ) e. RR )
386 25 33 remulcld 
 |-  ( ph -> ( ( X ` 2 ) x. ( Y ` 2 ) ) e. RR )
387 385 386 readdcld 
 |-  ( ph -> ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) e. RR )
388 39 42 remulcld 
 |-  ( ph -> ( ( X ` 3 ) x. ( Y ` 3 ) ) e. RR )
389 387 388 readdcld 
 |-  ( ph -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) e. RR )
390 389 adantr 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) e. RR )
391 348 ffvelcdmda 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( Z ` t ) e. RR )
392 390 391 remulcld 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) e. RR )
393 384 392 resubcld 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) e. RR )
394 10 376 361 393 fvmptd3 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) )
395 371 394 eqtr4d 
 |-  ( ( ph /\ t e. ( 1 ... 3 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) ` t ) )
396 8 12 395 eqfnfvd 
 |-  ( ph -> ( X crossp ( Y crossp Z ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) )