Metamath Proof Explorer

Theorem crossp3i

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, 1-Aug-2026)

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