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	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdotd.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdotd.3	$$⊢\phi \to C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspdotd	Could not format assertion : No typesetting found for |- ( ph -> ( 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		crosspdotd.1	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspdotd.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		crosspdotd.3	$$⊢\phi \to C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
4	1 2 3	crosspdot0lem	Could not format ( ph -> ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) ) : No typesetting found for |- ( ph -> ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) ) with typecode |-
5	1 2 3	crosspdotsumlem	Could not format ( ph -> ( 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 |- ( ph -> ( 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	crosspv1d	Could not format ( ph -> ( ( B crossp C ) ` 1 ) = ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) : No typesetting found for |- ( ph -> ( ( B crossp C ) ` 1 ) = ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) with typecode |-
7	6	oveq2d	Could not format ( ph -> ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) = ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( 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	crosspv2d	Could not format ( ph -> ( ( B crossp C ) ` 2 ) = ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) : No typesetting found for |- ( ph -> ( ( B crossp C ) ` 2 ) = ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) with typecode |-
9	8	oveq2d	Could not format ( ph -> ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) = ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( 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	crosspv3d	Could not format ( ph -> ( ( B crossp C ) ` 3 ) = ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) : No typesetting found for |- ( ph -> ( ( B crossp C ) ` 3 ) = ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) with typecode |-
11	10	oveq2d	Could not format ( ph -> ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) = ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( 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	oveq12d	Could not format ( ph -> ( ( ( 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 |- ( ph -> ( ( ( 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	oveq12d	Could not format ( ph -> ( ( ( 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 |- ( ph -> ( ( ( 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	rr3fv1cld	$$⊢\phi \to A\left(1\right)\in ℝ$$
15	14	recnd	$$⊢\phi \to A\left(1\right)\in ℂ$$
16	2	rr3fv2cld	$$⊢\phi \to B\left(2\right)\in ℝ$$
17	3	rr3fv3cld	$$⊢\phi \to C\left(3\right)\in ℝ$$
18	16 17	remulcld	$$⊢\phi \to B\left(2\right)C\left(3\right)\in ℝ$$
19	18	recnd	$$⊢\phi \to B\left(2\right)C\left(3\right)\in ℂ$$
20	2	rr3fv3cld	$$⊢\phi \to B\left(3\right)\in ℝ$$
21	3	rr3fv2cld	$$⊢\phi \to C\left(2\right)\in ℝ$$
22	20 21	remulcld	$$⊢\phi \to B\left(3\right)C\left(2\right)\in ℝ$$
23	22	recnd	$$⊢\phi \to B\left(3\right)C\left(2\right)\in ℂ$$
24	15 19 23	subdid	$$⊢\phi \to 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	recnd	$$⊢\phi \to B\left(2\right)\in ℂ$$
26	17	recnd	$$⊢\phi \to C\left(3\right)\in ℂ$$
27	15 25 26	mulassd	$$⊢\phi \to 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	eqcomd	$$⊢\phi \to 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	recnd	$$⊢\phi \to B\left(3\right)\in ℂ$$
30	21	recnd	$$⊢\phi \to C\left(2\right)\in ℂ$$
31	15 29 30	mulassd	$$⊢\phi \to 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	eqcomd	$$⊢\phi \to 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	oveq12d	$$⊢\phi \to 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	eqtrd	$$⊢\phi \to 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	rr3fv2cld	$$⊢\phi \to A\left(2\right)\in ℝ$$
36	35	recnd	$$⊢\phi \to A\left(2\right)\in ℂ$$
37	3	rr3fv1cld	$$⊢\phi \to C\left(1\right)\in ℝ$$
38	20 37	remulcld	$$⊢\phi \to B\left(3\right)C\left(1\right)\in ℝ$$
39	38	recnd	$$⊢\phi \to B\left(3\right)C\left(1\right)\in ℂ$$
40	2	rr3fv1cld	$$⊢\phi \to B\left(1\right)\in ℝ$$
41	40 17	remulcld	$$⊢\phi \to B\left(1\right)C\left(3\right)\in ℝ$$
42	41	recnd	$$⊢\phi \to B\left(1\right)C\left(3\right)\in ℂ$$
43	36 39 42	subdid	$$⊢\phi \to 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	recnd	$$⊢\phi \to C\left(1\right)\in ℂ$$
45	36 29 44	mulassd	$$⊢\phi \to 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	eqcomd	$$⊢\phi \to 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	recnd	$$⊢\phi \to B\left(1\right)\in ℂ$$
48	36 47 26	mulassd	$$⊢\phi \to 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	eqcomd	$$⊢\phi \to 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	oveq12d	$$⊢\phi \to 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	eqtrd	$$⊢\phi \to 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	rr3fv3cld	$$⊢\phi \to A\left(3\right)\in ℝ$$
53	52	recnd	$$⊢\phi \to A\left(3\right)\in ℂ$$
54	40 21	remulcld	$$⊢\phi \to B\left(1\right)C\left(2\right)\in ℝ$$
55	54	recnd	$$⊢\phi \to B\left(1\right)C\left(2\right)\in ℂ$$
56	16 37	remulcld	$$⊢\phi \to B\left(2\right)C\left(1\right)\in ℝ$$
57	56	recnd	$$⊢\phi \to B\left(2\right)C\left(1\right)\in ℂ$$
58	53 55 57	subdid	$$⊢\phi \to 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	mulassd	$$⊢\phi \to 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	eqcomd	$$⊢\phi \to 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	mulassd	$$⊢\phi \to 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	eqcomd	$$⊢\phi \to 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	oveq12d	$$⊢\phi \to 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	eqtrd	$$⊢\phi \to 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	oveq12d	$$⊢\phi \to 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	oveq12d	$$⊢\phi \to 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	eqtrd	Could not format ( ph -> ( ( ( 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 |- ( ph -> ( ( ( 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	eqtrd	Could not format ( ph -> ( 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 |- ( ph -> ( 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	eqtrd	Could not format ( ph -> ( 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 |- ( ph -> ( 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 |-