Metamath Proof Explorer

Theorem crosspdotd

Description: Value of the scalar triple product, expanded into the standard six-term Sarrus polynomial. (Contributed by Jiamin Zhao, 12-Aug-2026)

Ref Expression
Hypotheses crosspdotd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
crosspdotd.2 ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
crosspdotd.3 ⊢ ( 𝜑 → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion crosspdotd ( 𝜑 → ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) + ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 crosspdotd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2 crosspdotd.2 ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
3 crosspdotd.3 ⊢ ( 𝜑 → 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
4 1 2 3 crosspdot0lem ⊢ ( 𝜑 → ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) )
5 1 2 3 crosspdotsumlem ⊢ ( 𝜑 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) )
6 2 3 crosspv1d ⊢ ( 𝜑 → ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) = ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) )
7 6 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) )
8 2 3 crosspv2d ⊢ ( 𝜑 → ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) = ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) )
9 8 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) )
10 2 3 crosspv3d ⊢ ( 𝜑 → ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) = ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) )
11 10 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) )
12 9 11 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) ) )
13 7 12 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) ) ) )
14 1 rr3fv1cld ⊢ ( 𝜑 → ( 𝐴 ‘ 1 ) ∈ ℝ )
15 14 recnd ⊢ ( 𝜑 → ( 𝐴 ‘ 1 ) ∈ ℂ )
16 2 rr3fv2cld ⊢ ( 𝜑 → ( 𝐵 ‘ 2 ) ∈ ℝ )
17 3 rr3fv3cld ⊢ ( 𝜑 → ( 𝐶 ‘ 3 ) ∈ ℝ )
18 16 17 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ∈ ℂ )
20 2 rr3fv3cld ⊢ ( 𝜑 → ( 𝐵 ‘ 3 ) ∈ ℝ )
21 3 rr3fv2cld ⊢ ( 𝜑 → ( 𝐶 ‘ 2 ) ∈ ℝ )
22 20 21 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ∈ ℂ )
24 15 19 23 subdid ⊢ ( 𝜑 → ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) − ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) )
25 16 recnd ⊢ ( 𝜑 → ( 𝐵 ‘ 2 ) ∈ ℂ )
26 17 recnd ⊢ ( 𝜑 → ( 𝐶 ‘ 3 ) ∈ ℂ )
27 15 25 26 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) )
28 27 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) )
29 20 recnd ⊢ ( 𝜑 → ( 𝐵 ‘ 3 ) ∈ ℂ )
30 21 recnd ⊢ ( 𝜑 → ( 𝐶 ‘ 2 ) ∈ ℂ )
31 15 29 30 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) )
32 31 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) )
33 28 32 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) − ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) = ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) )
34 24 33 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) = ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) )
35 1 rr3fv2cld ⊢ ( 𝜑 → ( 𝐴 ‘ 2 ) ∈ ℝ )
36 35 recnd ⊢ ( 𝜑 → ( 𝐴 ‘ 2 ) ∈ ℂ )
37 3 rr3fv1cld ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ∈ ℝ )
38 20 37 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ∈ ℝ )
39 38 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ∈ ℂ )
40 2 rr3fv1cld ⊢ ( 𝜑 → ( 𝐵 ‘ 1 ) ∈ ℝ )
41 40 17 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ∈ ℝ )
42 41 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ∈ ℂ )
43 36 39 42 subdid ⊢ ( 𝜑 → ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) − ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) )
44 37 recnd ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ∈ ℂ )
45 36 29 44 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) )
46 45 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) )
47 40 recnd ⊢ ( 𝜑 → ( 𝐵 ‘ 1 ) ∈ ℂ )
48 36 47 26 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) )
49 48 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) )
50 46 49 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) − ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) = ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) )
51 43 50 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) = ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) )
52 1 rr3fv3cld ⊢ ( 𝜑 → ( 𝐴 ‘ 3 ) ∈ ℝ )
53 52 recnd ⊢ ( 𝜑 → ( 𝐴 ‘ 3 ) ∈ ℂ )
54 40 21 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ∈ ℝ )
55 54 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ∈ ℂ )
56 16 37 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ∈ ℝ )
57 56 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ∈ ℂ )
58 53 55 57 subdid ⊢ ( 𝜑 → ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) − ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) )
59 53 47 30 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) )
60 59 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) )
61 53 25 44 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) )
62 61 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) )
63 60 62 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) − ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) = ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) )
64 58 63 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) = ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) )
65 51 64 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) ) = ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) )
66 34 65 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) ) ) = ( ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) + ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) ) )
67 13 66 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) = ( ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) + ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) ) )
68 5 67 eqtrd ⊢ ( 𝜑 → ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) + ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) ) )
69 4 68 eqtrd ⊢ ( 𝜑 → ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) + ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) ) )