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	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdoti.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdoti.3	$$⊢C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspdoti	Could not format assertion : No typesetting found for |- ( B ( tripp ` A ) C ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		crosspdoti.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspdoti.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		crosspdoti.3	$$⊢C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
4	1 2 3	crosspdot0i	Could not format ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) : No typesetting found for |- ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) with typecode |-
5	1 2 3	crosspdotsumi	Could not format ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) : No typesetting found for |- ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) with typecode |-
6	2 3	crosspv1i	Could not format ( ( B crossp C ) ` 1 ) = ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) : No typesetting found for |- ( ( B crossp C ) ` 1 ) = ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) with typecode |-
7	6	oveq2i	Could not format ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) = ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) : No typesetting found for |- ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) = ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) with typecode |-
8	2 3	crosspv2i	Could not format ( ( B crossp C ) ` 2 ) = ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) : No typesetting found for |- ( ( B crossp C ) ` 2 ) = ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) with typecode |-
9	8	oveq2i	Could not format ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) = ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) : No typesetting found for |- ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) = ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) with typecode |-
10	2 3	crosspv3i	Could not format ( ( B crossp C ) ` 3 ) = ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) : No typesetting found for |- ( ( B crossp C ) ` 3 ) = ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) with typecode |-
11	10	oveq2i	Could not format ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) = ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) : No typesetting found for |- ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) = ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) with typecode |-
12	9 11	oveq12i	Could not format ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) = ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) : No typesetting found for |- ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) = ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) with typecode |-
13	7 12	oveq12i	Could not format ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) = ( ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) + ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) ) : No typesetting found for |- ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) = ( ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) + ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) ) with typecode |-
14	1	rr3fv1cli	$$⊢A\left(1\right)\in ℝ$$
15	14	recni	$$⊢A\left(1\right)\in ℂ$$
16	2	rr3fv2cli	$$⊢B\left(2\right)\in ℝ$$
17	3	rr3fv3cli	$$⊢C\left(3\right)\in ℝ$$
18	16 17	remulcli	$$⊢B\left(2\right)C\left(3\right)\in ℝ$$
19	18	recni	$$⊢B\left(2\right)C\left(3\right)\in ℂ$$
20	2	rr3fv3cli	$$⊢B\left(3\right)\in ℝ$$
21	3	rr3fv2cli	$$⊢C\left(2\right)\in ℝ$$
22	20 21	remulcli	$$⊢B\left(3\right)C\left(2\right)\in ℝ$$
23	22	recni	$$⊢B\left(3\right)C\left(2\right)\in ℂ$$
24	15 19 23	subdii	$$⊢A\left(1\right)\left(B\left(2\right)C\left(3\right)-B\left(3\right)C\left(2\right)\right)=A\left(1\right)B\left(2\right)C\left(3\right)-A\left(1\right)B\left(3\right)C\left(2\right)$$
25	16	recni	$$⊢B\left(2\right)\in ℂ$$
26	17	recni	$$⊢C\left(3\right)\in ℂ$$
27	15 25 26	mulassi	$$⊢A\left(1\right)B\left(2\right)C\left(3\right)=A\left(1\right)B\left(2\right)C\left(3\right)$$
28	27	eqcomi	$$⊢A\left(1\right)B\left(2\right)C\left(3\right)=A\left(1\right)B\left(2\right)C\left(3\right)$$
29	20	recni	$$⊢B\left(3\right)\in ℂ$$
30	21	recni	$$⊢C\left(2\right)\in ℂ$$
31	15 29 30	mulassi	$$⊢A\left(1\right)B\left(3\right)C\left(2\right)=A\left(1\right)B\left(3\right)C\left(2\right)$$
32	31	eqcomi	$$⊢A\left(1\right)B\left(3\right)C\left(2\right)=A\left(1\right)B\left(3\right)C\left(2\right)$$
33	28 32	oveq12i	$$⊢A\left(1\right)B\left(2\right)C\left(3\right)-A\left(1\right)B\left(3\right)C\left(2\right)=A\left(1\right)B\left(2\right)C\left(3\right)-A\left(1\right)B\left(3\right)C\left(2\right)$$
34	24 33	eqtri	$$⊢A\left(1\right)\left(B\left(2\right)C\left(3\right)-B\left(3\right)C\left(2\right)\right)=A\left(1\right)B\left(2\right)C\left(3\right)-A\left(1\right)B\left(3\right)C\left(2\right)$$
35	1	rr3fv2cli	$$⊢A\left(2\right)\in ℝ$$
36	35	recni	$$⊢A\left(2\right)\in ℂ$$
37	3	rr3fv1cli	$$⊢C\left(1\right)\in ℝ$$
38	20 37	remulcli	$$⊢B\left(3\right)C\left(1\right)\in ℝ$$
39	38	recni	$$⊢B\left(3\right)C\left(1\right)\in ℂ$$
40	2	rr3fv1cli	$$⊢B\left(1\right)\in ℝ$$
41	40 17	remulcli	$$⊢B\left(1\right)C\left(3\right)\in ℝ$$
42	41	recni	$$⊢B\left(1\right)C\left(3\right)\in ℂ$$
43	36 39 42	subdii	$$⊢A\left(2\right)\left(B\left(3\right)C\left(1\right)-B\left(1\right)C\left(3\right)\right)=A\left(2\right)B\left(3\right)C\left(1\right)-A\left(2\right)B\left(1\right)C\left(3\right)$$
44	37	recni	$$⊢C\left(1\right)\in ℂ$$
45	36 29 44	mulassi	$$⊢A\left(2\right)B\left(3\right)C\left(1\right)=A\left(2\right)B\left(3\right)C\left(1\right)$$
46	45	eqcomi	$$⊢A\left(2\right)B\left(3\right)C\left(1\right)=A\left(2\right)B\left(3\right)C\left(1\right)$$
47	40	recni	$$⊢B\left(1\right)\in ℂ$$
48	36 47 26	mulassi	$$⊢A\left(2\right)B\left(1\right)C\left(3\right)=A\left(2\right)B\left(1\right)C\left(3\right)$$
49	48	eqcomi	$$⊢A\left(2\right)B\left(1\right)C\left(3\right)=A\left(2\right)B\left(1\right)C\left(3\right)$$
50	46 49	oveq12i	$$⊢A\left(2\right)B\left(3\right)C\left(1\right)-A\left(2\right)B\left(1\right)C\left(3\right)=A\left(2\right)B\left(3\right)C\left(1\right)-A\left(2\right)B\left(1\right)C\left(3\right)$$
51	43 50	eqtri	$$⊢A\left(2\right)\left(B\left(3\right)C\left(1\right)-B\left(1\right)C\left(3\right)\right)=A\left(2\right)B\left(3\right)C\left(1\right)-A\left(2\right)B\left(1\right)C\left(3\right)$$
52	1	rr3fv3cli	$$⊢A\left(3\right)\in ℝ$$
53	52	recni	$$⊢A\left(3\right)\in ℂ$$
54	40 21	remulcli	$$⊢B\left(1\right)C\left(2\right)\in ℝ$$
55	54	recni	$$⊢B\left(1\right)C\left(2\right)\in ℂ$$
56	16 37	remulcli	$$⊢B\left(2\right)C\left(1\right)\in ℝ$$
57	56	recni	$$⊢B\left(2\right)C\left(1\right)\in ℂ$$
58	53 55 57	subdii	$$⊢A\left(3\right)\left(B\left(1\right)C\left(2\right)-B\left(2\right)C\left(1\right)\right)=A\left(3\right)B\left(1\right)C\left(2\right)-A\left(3\right)B\left(2\right)C\left(1\right)$$
59	53 47 30	mulassi	$$⊢A\left(3\right)B\left(1\right)C\left(2\right)=A\left(3\right)B\left(1\right)C\left(2\right)$$
60	59	eqcomi	$$⊢A\left(3\right)B\left(1\right)C\left(2\right)=A\left(3\right)B\left(1\right)C\left(2\right)$$
61	53 25 44	mulassi	$$⊢A\left(3\right)B\left(2\right)C\left(1\right)=A\left(3\right)B\left(2\right)C\left(1\right)$$
62	61	eqcomi	$$⊢A\left(3\right)B\left(2\right)C\left(1\right)=A\left(3\right)B\left(2\right)C\left(1\right)$$
63	60 62	oveq12i	$$⊢A\left(3\right)B\left(1\right)C\left(2\right)-A\left(3\right)B\left(2\right)C\left(1\right)=A\left(3\right)B\left(1\right)C\left(2\right)-A\left(3\right)B\left(2\right)C\left(1\right)$$
64	58 63	eqtri	$$⊢A\left(3\right)\left(B\left(1\right)C\left(2\right)-B\left(2\right)C\left(1\right)\right)=A\left(3\right)B\left(1\right)C\left(2\right)-A\left(3\right)B\left(2\right)C\left(1\right)$$
65	51 64	oveq12i	$$⊢A\left(2\right)\left(B\left(3\right)C\left(1\right)-B\left(1\right)C\left(3\right)\right)+A\left(3\right)\left(B\left(1\right)C\left(2\right)-B\left(2\right)C\left(1\right)\right)=\left(A\left(2\right)B\left(3\right)C\left(1\right)-A\left(2\right)B\left(1\right)C\left(3\right)\right)+A\left(3\right)B\left(1\right)C\left(2\right)-A\left(3\right)B\left(2\right)C\left(1\right)$$
66	34 65	oveq12i	$$⊢A\left(1\right)\left(B\left(2\right)C\left(3\right)-B\left(3\right)C\left(2\right)\right)+A\left(2\right)\left(B\left(3\right)C\left(1\right)-B\left(1\right)C\left(3\right)\right)+A\left(3\right)\left(B\left(1\right)C\left(2\right)-B\left(2\right)C\left(1\right)\right)=\left(A\left(1\right)B\left(2\right)C\left(3\right)-A\left(1\right)B\left(3\right)C\left(2\right)\right)+\left(A\left(2\right)B\left(3\right)C\left(1\right)-A\left(2\right)B\left(1\right)C\left(3\right)\right)+\left(A\left(3\right)B\left(1\right)C\left(2\right)-A\left(3\right)B\left(2\right)C\left(1\right)\right)$$
67	13 66	eqtri	Could not format ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) : No typesetting found for |- ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) with typecode |-
68	5 67	eqtri	Could not format ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) : No typesetting found for |- ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) with typecode |-
69	4 68	eqtri	Could not format ( B ( tripp ` A ) C ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) : No typesetting found for |- ( B ( tripp ` A ) C ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) ) with typecode |-