Theorem crosspdot0i

Description: Unfold the curried scalar triple product application into an explicit group sum. (A helper for crosspdoti .) (Contributed by Jiamin Zhao, 1-Aug-2026)

	Ref	Expression
Hypotheses	crosspdot0i.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdot0i.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdot0i.3	$$⊢C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspdot0i	Could not format assertion : No typesetting found for |- ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		crosspdot0i.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspdot0i.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		crosspdot0i.3	$$⊢C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
4		ovex	$$⊢{ℝ}^{\left(1\dots 3\right)}\in \mathrm{V}$$
5	4 4	mpoex	Could not format ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) e. _V : No typesetting found for |- ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) e. _V with typecode |-
6		fveq1	$$⊢s=A\to s\left(k\right)=A\left(k\right)$$
7	6	oveq1d	Could not format ( s = A -> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) : No typesetting found for |- ( s = A -> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) with typecode |-
8	7	mpteq2dv	Could not format ( s = A -> ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) = ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) : No typesetting found for |- ( s = A -> ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) = ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) with typecode |-
9	8	oveq2d	Could not format ( s = A -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) : No typesetting found for |- ( s = A -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) with typecode |-
10	9	mpoeq3dv	Could not format ( s = A -> ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) : No typesetting found for |- ( s = A -> ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) with typecode |-
11		df-tripp	Could not format tripp = ( s e. ( RR ^m ( 1 ... 3 ) ) |-> ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) : No typesetting found for |- tripp = ( s e. ( RR ^m ( 1 ... 3 ) ) |-> ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) with typecode |-
12	10 11	fvmptg	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) e. _V ) -> ( tripp ` A ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) e. _V ) -> ( tripp ` A ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) with typecode |-
13	1 5 12	mp2an	Could not format ( tripp ` A ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) : No typesetting found for |- ( tripp ` A ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) with typecode |-
14	13	oveqi	Could not format ( B ( tripp ` A ) C ) = ( B ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) C ) : No typesetting found for |- ( B ( tripp ` A ) C ) = ( B ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) C ) with typecode |-
15		eqidd	Could not format ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) : No typesetting found for |- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) = ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) ) with typecode |-
16		simprl	$$⊢\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge \left(w=B\wedge z=C\right)\right)\to w=B$$
17		simprr	$$⊢\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge \left(w=B\wedge z=C\right)\right)\to z=C$$
18	16 17	oveq12d	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( w crossp z ) = ( B crossp C ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( w crossp z ) = ( B crossp C ) ) with typecode |-
19	18	fveq1d	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( ( w crossp z ) ` k ) = ( ( B crossp C ) ` k ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( ( w crossp z ) ` k ) = ( ( B crossp C ) ` k ) ) with typecode |-
20	19	oveq2d	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) with typecode |-
21	20	mpteq2dv	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) = ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) = ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) with typecode |-
22	21	oveq2d	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) ) with typecode |-
23	2	a1i	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
24	3	a1i	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\to C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
25		ovexd	Could not format ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) e. _V ) : No typesetting found for |- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) e. _V ) with typecode |-
26	15 22 23 24 25	ovmpod	Could not format ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( B ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) ) : No typesetting found for |- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( B ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) ) with typecode |-
27	1 26	ax-mp	Could not format ( B ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) : No typesetting found for |- ( B ( w e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) ) ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) with typecode |-
28	14 27	eqtri	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 |-