Metamath Proof Explorer

Theorem crosspaltd

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

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

Proof

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