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

Proof

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