Metamath Proof Explorer

Theorem crosspalti

Description: Antisymmetry of the cross product: swapping the two vectors negates the result. (Contributed by Jiamin Zhao, 1-Aug-2026)

Ref Expression
Hypotheses crosspalti.1 
|- A e. ( RR ^m ( 1 ... 3 ) )
crosspalti.2 
|- B e. ( RR ^m ( 1 ... 3 ) )
Assertion crosspalti 
|- ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) )

Proof

Step Hyp Ref Expression
1 crosspalti.1 
 |-  A e. ( RR ^m ( 1 ... 3 ) )
2 crosspalti.2 
 |-  B e. ( RR ^m ( 1 ... 3 ) )
3 1 2 crosspcli 
 |-  ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) )
4 elmapfn 
 |-  ( ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) Fn ( 1 ... 3 ) )
5 3 4 ax-mp 
 |-  ( A crossp B ) Fn ( 1 ... 3 )
6 5 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) Fn ( 1 ... 3 ) )
7 negex 
 |-  -u ( ( B crossp A ) ` k ) e. _V
8 eqid 
 |-  ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) )
9 7 8 fnmpti 
 |-  ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) Fn ( 1 ... 3 )
10 9 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) Fn ( 1 ... 3 ) )
11 simpr 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> t = 1 )
12 11 fveq2d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 1 ) )
13 1 2 crosspv1i 
 |-  ( ( A crossp B ) ` 1 ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) )
14 12 13 eqtrdi 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) )
15 1 rr3fv2cli 
 |-  ( A ` 2 ) e. RR
16 15 recni 
 |-  ( A ` 2 ) e. CC
17 2 rr3fv3cli 
 |-  ( B ` 3 ) e. RR
18 17 recni 
 |-  ( B ` 3 ) e. CC
19 16 18 mulcomi 
 |-  ( ( A ` 2 ) x. ( B ` 3 ) ) = ( ( B ` 3 ) x. ( A ` 2 ) )
20 19 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A ` 2 ) x. ( B ` 3 ) ) = ( ( B ` 3 ) x. ( A ` 2 ) ) )
21 1 rr3fv3cli 
 |-  ( A ` 3 ) e. RR
22 21 recni 
 |-  ( A ` 3 ) e. CC
23 2 rr3fv2cli 
 |-  ( B ` 2 ) e. RR
24 23 recni 
 |-  ( B ` 2 ) e. CC
25 22 24 mulcomi 
 |-  ( ( A ` 3 ) x. ( B ` 2 ) ) = ( ( B ` 2 ) x. ( A ` 3 ) )
26 25 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A ` 3 ) x. ( B ` 2 ) ) = ( ( B ` 2 ) x. ( A ` 3 ) ) )
27 20 26 oveq12d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) = ( ( ( B ` 3 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 3 ) ) ) )
28 23 21 remulcli 
 |-  ( ( B ` 2 ) x. ( A ` 3 ) ) e. RR
29 28 recni 
 |-  ( ( B ` 2 ) x. ( A ` 3 ) ) e. CC
30 17 15 remulcli 
 |-  ( ( B ` 3 ) x. ( A ` 2 ) ) e. RR
31 30 recni 
 |-  ( ( B ` 3 ) x. ( A ` 2 ) ) e. CC
32 29 31 negsubdi2i 
 |-  -u ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) = ( ( ( B ` 3 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 3 ) ) )
33 27 32 eqtr4di 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) = -u ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) )
34 11 fveq2d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 1 ) )
35 2 1 crosspv1i 
 |-  ( ( B crossp A ) ` 1 ) = ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) )
36 34 35 eqtrdi 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( B crossp A ) ` t ) = ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) )
37 36 negeqd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> -u ( ( B crossp A ) ` t ) = -u ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) )
38 33 37 eqtr4d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) = -u ( ( B crossp A ) ` t ) )
39 14 38 eqtrd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) )
40 2 1 crosspv2i 
 |-  ( ( B crossp A ) ` 2 ) = ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) )
41 40 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B crossp A ) ` 2 ) = ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) )
42 41 negeqd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = -u ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) )
43 1 rr3fv1cli 
 |-  ( A ` 1 ) e. RR
44 17 43 remulcli 
 |-  ( ( B ` 3 ) x. ( A ` 1 ) ) e. RR
45 44 recni 
 |-  ( ( B ` 3 ) x. ( A ` 1 ) ) e. CC
46 2 rr3fv1cli 
 |-  ( B ` 1 ) e. RR
47 remulcl 
 |-  ( ( ( B ` 1 ) e. RR /\ ( A ` 3 ) e. RR ) -> ( ( B ` 1 ) x. ( A ` 3 ) ) e. RR )
48 47 recnd 
 |-  ( ( ( B ` 1 ) e. RR /\ ( A ` 3 ) e. RR ) -> ( ( B ` 1 ) x. ( A ` 3 ) ) e. CC )
49 46 21 48 mp2an 
 |-  ( ( B ` 1 ) x. ( A ` 3 ) ) e. CC
50 45 49 negsubdi2i 
 |-  -u ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) = ( ( ( B ` 1 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 1 ) ) )
51 46 recni 
 |-  ( B ` 1 ) e. CC
52 51 22 mulcomi 
 |-  ( ( B ` 1 ) x. ( A ` 3 ) ) = ( ( A ` 3 ) x. ( B ` 1 ) )
53 52 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B ` 1 ) x. ( A ` 3 ) ) = ( ( A ` 3 ) x. ( B ` 1 ) ) )
54 43 recni 
 |-  ( A ` 1 ) e. CC
55 18 54 mulcomi 
 |-  ( ( B ` 3 ) x. ( A ` 1 ) ) = ( ( A ` 1 ) x. ( B ` 3 ) )
56 55 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B ` 3 ) x. ( A ` 1 ) ) = ( ( A ` 1 ) x. ( B ` 3 ) ) )
57 53 56 oveq12d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( B ` 1 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 1 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) )
58 50 57 eqtrid 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) )
59 42 58 eqtrd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) )
60 1 2 crosspv2i 
 |-  ( ( A crossp B ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) )
61 59 60 eqtr4di 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = ( ( A crossp B ) ` 2 ) )
62 simpr 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> t = ( 1 + 1 ) )
63 1p1e2 
 |-  ( 1 + 1 ) = 2
64 62 63 eqtrdi 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> t = 2 )
65 64 fveq2d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 2 ) )
66 65 negeqd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` t ) = -u ( ( B crossp A ) ` 2 ) )
67 64 fveq2d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 2 ) )
68 61 66 67 3eqtr4rd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) )
69 2 1 crosspv3i 
 |-  ( ( B crossp A ) ` 3 ) = ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) )
70 69 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B crossp A ) ` 3 ) = ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) )
71 70 negeqd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = -u ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) )
72 46 15 remulcli 
 |-  ( ( B ` 1 ) x. ( A ` 2 ) ) e. RR
73 72 recni 
 |-  ( ( B ` 1 ) x. ( A ` 2 ) ) e. CC
74 remulcl 
 |-  ( ( ( B ` 2 ) e. RR /\ ( A ` 1 ) e. RR ) -> ( ( B ` 2 ) x. ( A ` 1 ) ) e. RR )
75 74 recnd 
 |-  ( ( ( B ` 2 ) e. RR /\ ( A ` 1 ) e. RR ) -> ( ( B ` 2 ) x. ( A ` 1 ) ) e. CC )
76 23 43 75 mp2an 
 |-  ( ( B ` 2 ) x. ( A ` 1 ) ) e. CC
77 73 76 negsubdi2i 
 |-  -u ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) = ( ( ( B ` 2 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 2 ) ) )
78 24 54 mulcomi 
 |-  ( ( B ` 2 ) x. ( A ` 1 ) ) = ( ( A ` 1 ) x. ( B ` 2 ) )
79 78 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B ` 2 ) x. ( A ` 1 ) ) = ( ( A ` 1 ) x. ( B ` 2 ) ) )
80 51 16 mulcomi 
 |-  ( ( B ` 1 ) x. ( A ` 2 ) ) = ( ( A ` 2 ) x. ( B ` 1 ) )
81 80 a1i 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B ` 1 ) x. ( A ` 2 ) ) = ( ( A ` 2 ) x. ( B ` 1 ) ) )
82 79 81 oveq12d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( B ` 2 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 2 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
83 77 82 eqtrid 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
84 71 83 eqtrd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
85 1 2 crosspv3i 
 |-  ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) )
86 84 85 eqtr4di 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = ( ( A crossp B ) ` 3 ) )
87 simpr 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> t = ( 1 + 2 ) )
88 1p2e3 
 |-  ( 1 + 2 ) = 3
89 87 88 eqtrdi 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> t = 3 )
90 89 fveq2d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 3 ) )
91 90 negeqd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` t ) = -u ( ( B crossp A ) ` 3 ) )
92 89 fveq2d 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 3 ) )
93 86 91 92 3eqtr4rd 
 |-  ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) )
94 simpr 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> t e. ( 1 ... 3 ) )
95 88 eqcomi 
 |-  3 = ( 1 + 2 )
96 95 oveq2i 
 |-  ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
97 1z 
 |-  1 e. ZZ
98 fztp 
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
99 97 98 ax-mp 
 |-  ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
100 96 99 eqtri 
 |-  ( 1 ... 3 ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
101 94 100 eleqtrdi 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> t e. { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
102 eltpi 
 |-  ( t e. { 1 , ( 1 + 1 ) , ( 1 + 2 ) } -> ( t = 1 \/ t = ( 1 + 1 ) \/ t = ( 1 + 2 ) ) )
103 101 102 syl 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( t = 1 \/ t = ( 1 + 1 ) \/ t = ( 1 + 2 ) ) )
104 39 68 93 103 mpjao3dan 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) )
105 fveq2 
 |-  ( k = t -> ( ( B crossp A ) ` k ) = ( ( B crossp A ) ` t ) )
106 105 negeqd 
 |-  ( k = t -> -u ( ( B crossp A ) ` k ) = -u ( ( B crossp A ) ` t ) )
107 negex 
 |-  -u ( ( B crossp A ) ` t ) e. _V
108 107 a1i 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> -u ( ( B crossp A ) ` t ) e. _V )
109 8 106 94 108 fvmptd3 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ` t ) = -u ( ( B crossp A ) ` t ) )
110 104 109 eqtr4d 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( A crossp B ) ` t ) = ( ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ` t ) )
111 6 10 110 eqfnfvd 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) )
112 1 111 ax-mp 
 |-  ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) )