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 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
crosspalti.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
Assertion crosspalti ( 𝐴 ⊠ 𝐵 ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 crosspalti.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
2 crosspalti.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
3 1 2 crosspcli ⊢ ( 𝐴 ⊠ 𝐵 ) ∈ ( ℝ ↑m ( 1 ... 3 ) )
4 elmapfn ⊢ ( ( 𝐴 ⊠ 𝐵 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐴 ⊠ 𝐵 ) Fn ( 1 ... 3 ) )
5 3 4 ax-mp ⊢ ( 𝐴 ⊠ 𝐵 ) Fn ( 1 ... 3 )
6 5 a1i ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐴 ⊠ 𝐵 ) Fn ( 1 ... 3 ) )
7 negex ⊢ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ∈ V
8 eqid ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) )
9 7 8 fnmpti ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ) Fn ( 1 ... 3 )
10 9 a1i ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ) Fn ( 1 ... 3 ) )
11 simpr ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → 𝑡 = 1 )
12 11 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = ( ( 𝐴 ⊠ 𝐵 ) ‘ 1 ) )
13 1 2 crosspv1i ⊢ ( ( 𝐴 ⊠ 𝐵 ) ‘ 1 ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) )
14 12 13 eqtrdi ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) )
15 1 rr3fv2cli ⊢ ( 𝐴 ‘ 2 ) ∈ ℝ
16 15 recni ⊢ ( 𝐴 ‘ 2 ) ∈ ℂ
17 2 rr3fv3cli ⊢ ( 𝐵 ‘ 3 ) ∈ ℝ
18 17 recni ⊢ ( 𝐵 ‘ 3 ) ∈ ℂ
19 16 18 mulcomi ⊢ ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) = ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) )
20 19 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) = ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) )
21 1 rr3fv3cli ⊢ ( 𝐴 ‘ 3 ) ∈ ℝ
22 21 recni ⊢ ( 𝐴 ‘ 3 ) ∈ ℂ
23 2 rr3fv2cli ⊢ ( 𝐵 ‘ 2 ) ∈ ℝ
24 23 recni ⊢ ( 𝐵 ‘ 2 ) ∈ ℂ
25 22 24 mulcomi ⊢ ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) = ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) )
26 25 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) = ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) )
27 20 26 oveq12d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) = ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) ) )
28 23 21 remulcli ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) ∈ ℝ
29 28 recni ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) ∈ ℂ
30 17 15 remulcli ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) ∈ ℝ
31 30 recni ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) ∈ ℂ
32 29 31 negsubdi2i ⊢ - ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) ) = ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) )
33 27 32 eqtr4di ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) = - ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) ) )
34 11 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = ( ( 𝐵 ⊠ 𝐴 ) ‘ 1 ) )
35 2 1 crosspv1i ⊢ ( ( 𝐵 ⊠ 𝐴 ) ‘ 1 ) = ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) )
36 34 35 eqtrdi ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) ) )
37 36 negeqd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = - ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 2 ) ) ) )
38 33 37 eqtr4d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
39 14 38 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = 1 ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
40 2 1 crosspv2i ⊢ ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) = ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) )
41 40 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) = ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ) )
42 41 negeqd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) = - ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ) )
43 1 rr3fv1cli ⊢ ( 𝐴 ‘ 1 ) ∈ ℝ
44 17 43 remulcli ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) ∈ ℝ
45 44 recni ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) ∈ ℂ
46 2 rr3fv1cli ⊢ ( 𝐵 ‘ 1 ) ∈ ℝ
47 remulcl ⊢ ( ( ( 𝐵 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) → ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ∈ ℝ )
48 47 recnd ⊢ ( ( ( 𝐵 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) → ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ∈ ℂ )
49 46 21 48 mp2an ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ∈ ℂ
50 45 49 negsubdi2i ⊢ - ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ) = ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) )
51 46 recni ⊢ ( 𝐵 ‘ 1 ) ∈ ℂ
52 51 22 mulcomi ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) = ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) )
53 52 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) = ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) )
54 43 recni ⊢ ( 𝐴 ‘ 1 ) ∈ ℂ
55 18 54 mulcomi ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) )
56 55 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) )
57 53 56 oveq12d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) )
58 50 57 eqtrid ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → - ( ( ( 𝐵 ‘ 3 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) )
59 42 58 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) )
60 1 2 crosspv2i ⊢ ( ( 𝐴 ⊠ 𝐵 ) ‘ 2 ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) )
61 59 60 eqtr4di ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) = ( ( 𝐴 ⊠ 𝐵 ) ‘ 2 ) )
62 simpr ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → 𝑡 = ( 1 + 1 ) )
63 1p1e2 ⊢ ( 1 + 1 ) = 2
64 62 63 eqtrdi ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → 𝑡 = 2 )
65 64 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) )
66 65 negeqd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 2 ) )
67 64 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = ( ( 𝐴 ⊠ 𝐵 ) ‘ 2 ) )
68 61 66 67 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 1 ) ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
69 2 1 crosspv3i ⊢ ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) = ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) )
70 69 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) = ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ) )
71 70 negeqd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) = - ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ) )
72 46 15 remulcli ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) ∈ ℝ
73 72 recni ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) ∈ ℂ
74 remulcl ⊢ ( ( ( 𝐵 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 1 ) ∈ ℝ ) → ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ∈ ℝ )
75 74 recnd ⊢ ( ( ( 𝐵 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 1 ) ∈ ℝ ) → ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ∈ ℂ )
76 23 43 75 mp2an ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ∈ ℂ
77 73 76 negsubdi2i ⊢ - ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ) = ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) )
78 24 54 mulcomi ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) )
79 78 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) )
80 51 16 mulcomi ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) = ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) )
81 80 a1i ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) = ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) )
82 79 81 oveq12d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
83 77 82 eqtrid ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → - ( ( ( 𝐵 ‘ 1 ) · ( 𝐴 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐴 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
84 71 83 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
85 1 2 crosspv3i ⊢ ( ( 𝐴 ⊠ 𝐵 ) ‘ 3 ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) )
86 84 85 eqtr4di ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) = ( ( 𝐴 ⊠ 𝐵 ) ‘ 3 ) )
87 simpr ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → 𝑡 = ( 1 + 2 ) )
88 1p2e3 ⊢ ( 1 + 2 ) = 3
89 87 88 eqtrdi ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → 𝑡 = 3 )
90 89 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) )
91 90 negeqd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 3 ) )
92 89 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = ( ( 𝐴 ⊠ 𝐵 ) ‘ 3 ) )
93 86 91 92 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) ∧ 𝑡 = ( 1 + 2 ) ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
94 simpr ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → 𝑡 ∈ ( 1 ... 3 ) )
95 88 eqcomi ⊢ 3 = ( 1 + 2 )
96 95 oveq2i ⊢ ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
97 1z ⊢ 1 ∈ ℤ
98 fztp ⊢ ( 1 ∈ ℤ → ( 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 ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → 𝑡 ∈ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
102 eltpi ⊢ ( 𝑡 ∈ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } → ( 𝑡 = 1 ∨ 𝑡 = ( 1 + 1 ) ∨ 𝑡 = ( 1 + 2 ) ) )
103 101 102 syl ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → ( 𝑡 = 1 ∨ 𝑡 = ( 1 + 1 ) ∨ 𝑡 = ( 1 + 2 ) ) )
104 39 68 93 103 mpjao3dan ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
105 fveq2 ⊢ ( 𝑘 = 𝑡 → ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) = ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
106 105 negeqd ⊢ ( 𝑘 = 𝑡 → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
107 negex ⊢ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) ∈ V
108 107 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) ∈ V )
109 8 106 94 108 fvmptd3 ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → ( ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ) ‘ 𝑡 ) = - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑡 ) )
110 104 109 eqtr4d ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑡 ∈ ( 1 ... 3 ) ) → ( ( 𝐴 ⊠ 𝐵 ) ‘ 𝑡 ) = ( ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ) ‘ 𝑡 ) )
111 6 10 110 eqfnfvd ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐴 ⊠ 𝐵 ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) ) )
112 1 111 ax-mp ⊢ ( 𝐴 ⊠ 𝐵 ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ - ( ( 𝐵 ⊠ 𝐴 ) ‘ 𝑘 ) )