Metamath Proof Explorer

Theorem crosspdoti

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

Ref Expression
Hypotheses crosspdoti.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
crosspdoti.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
crosspdoti.3 ⊢ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) )
Assertion crosspdoti ( 𝐵 ( 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 crosspdoti.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
2 crosspdoti.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
3 crosspdoti.3 ⊢ 𝐶 ∈ ( ℝ ↑m ( 1 ... 3 ) )
4 1 2 3 crosspdot0i ⊢ ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) )
5 1 2 3 crosspdotsumi ⊢ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 𝑘 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) )
6 2 3 crosspv1i ⊢ ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) = ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) )
7 6 oveq2i ⊢ ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) )
8 2 3 crosspv2i ⊢ ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) = ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) )
9 8 oveq2i ⊢ ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) )
10 2 3 crosspv3i ⊢ ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) = ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) )
11 10 oveq2i ⊢ ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) )
12 9 11 oveq12i ⊢ ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) )
13 7 12 oveq12i ⊢ ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 1 ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 2 ) ) + ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ⊠ 𝐶 ) ‘ 3 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) + ( ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) + ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) ) )
14 1 rr3fv1cli ⊢ ( 𝐴 ‘ 1 ) ∈ ℝ
15 14 recni ⊢ ( 𝐴 ‘ 1 ) ∈ ℂ
16 2 rr3fv2cli ⊢ ( 𝐵 ‘ 2 ) ∈ ℝ
17 3 rr3fv3cli ⊢ ( 𝐶 ‘ 3 ) ∈ ℝ
18 16 17 remulcli ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ∈ ℝ
19 18 recni ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ∈ ℂ
20 2 rr3fv3cli ⊢ ( 𝐵 ‘ 3 ) ∈ ℝ
21 3 rr3fv2cli ⊢ ( 𝐶 ‘ 2 ) ∈ ℝ
22 20 21 remulcli ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ∈ ℝ
23 22 recni ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ∈ ℂ
24 15 19 23 subdii ⊢ ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) − ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) )
25 16 recni ⊢ ( 𝐵 ‘ 2 ) ∈ ℂ
26 17 recni ⊢ ( 𝐶 ‘ 3 ) ∈ ℂ
27 15 25 26 mulassi ⊢ ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) )
28 27 eqcomi ⊢ ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) )
29 20 recni ⊢ ( 𝐵 ‘ 3 ) ∈ ℂ
30 21 recni ⊢ ( 𝐶 ‘ 2 ) ∈ ℂ
31 15 29 30 mulassi ⊢ ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) = ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) )
32 31 eqcomi ⊢ ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) )
33 28 32 oveq12i ⊢ ( ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) ) − ( ( 𝐴 ‘ 1 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) = ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) )
34 24 33 eqtri ⊢ ( ( 𝐴 ‘ 1 ) · ( ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 3 ) ) − ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 2 ) ) ) ) = ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) )
35 1 rr3fv2cli ⊢ ( 𝐴 ‘ 2 ) ∈ ℝ
36 35 recni ⊢ ( 𝐴 ‘ 2 ) ∈ ℂ
37 3 rr3fv1cli ⊢ ( 𝐶 ‘ 1 ) ∈ ℝ
38 20 37 remulcli ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ∈ ℝ
39 38 recni ⊢ ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ∈ ℂ
40 2 rr3fv1cli ⊢ ( 𝐵 ‘ 1 ) ∈ ℝ
41 40 17 remulcli ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ∈ ℝ
42 41 recni ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ∈ ℂ
43 36 39 42 subdii ⊢ ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) − ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) )
44 37 recni ⊢ ( 𝐶 ‘ 1 ) ∈ ℂ
45 36 29 44 mulassi ⊢ ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) )
46 45 eqcomi ⊢ ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) )
47 40 recni ⊢ ( 𝐵 ‘ 1 ) ∈ ℂ
48 36 47 26 mulassi ⊢ ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) = ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) )
49 48 eqcomi ⊢ ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) )
50 46 49 oveq12i ⊢ ( ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) ) − ( ( 𝐴 ‘ 2 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) = ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) )
51 43 50 eqtri ⊢ ( ( 𝐴 ‘ 2 ) · ( ( ( 𝐵 ‘ 3 ) · ( 𝐶 ‘ 1 ) ) − ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 3 ) ) ) ) = ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) )
52 1 rr3fv3cli ⊢ ( 𝐴 ‘ 3 ) ∈ ℝ
53 52 recni ⊢ ( 𝐴 ‘ 3 ) ∈ ℂ
54 40 21 remulcli ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ∈ ℝ
55 54 recni ⊢ ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ∈ ℂ
56 16 37 remulcli ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ∈ ℝ
57 56 recni ⊢ ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ∈ ℂ
58 53 55 57 subdii ⊢ ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) − ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) )
59 53 47 30 mulassi ⊢ ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) )
60 59 eqcomi ⊢ ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) )
61 53 25 44 mulassi ⊢ ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) = ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) )
62 61 eqcomi ⊢ ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) )
63 60 62 oveq12i ⊢ ( ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) ) − ( ( 𝐴 ‘ 3 ) · ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) = ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) )
64 58 63 eqtri ⊢ ( ( 𝐴 ‘ 3 ) · ( ( ( 𝐵 ‘ 1 ) · ( 𝐶 ‘ 2 ) ) − ( ( 𝐵 ‘ 2 ) · ( 𝐶 ‘ 1 ) ) ) ) = ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) )
65 51 64 oveq12i ⊢ ( ( ( 𝐴 ‘ 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 oveq12i ⊢ ( ( ( 𝐴 ‘ 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 eqtri ⊢ ( ( ( 𝐴 ‘ 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 eqtri ⊢ ( ℝ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 eqtri ⊢ ( 𝐵 ( tripp ‘ 𝐴 ) 𝐶 ) = ( ( ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 3 ) ) − ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 2 ) ) ) + ( ( ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) · ( 𝐶 ‘ 1 ) ) − ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 3 ) ) ) + ( ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) · ( 𝐶 ‘ 2 ) ) − ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) · ( 𝐶 ‘ 1 ) ) ) ) )