Theorem crosspdot0lem

Description: Lemma for crosspdotd . Unfold the curried scalar triple product application into an explicit group sum. (Contributed by Jiamin Zhao, 12-Aug-2026)

	Ref	Expression
Hypotheses	crosspdot0lem.1	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdot0lem.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdot0lem.3	$$⊢\phi \to C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspdot0lem	Could not format assertion : No typesetting found for |- ( ph -> ( 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		crosspdot0lem.1	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspdot0lem.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		crosspdot0lem.3	$$⊢\phi \to C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
4		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 |-
5		fveq1	$$⊢s=A\to s\left(k\right)=A\left(k\right)$$
6	5	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 |-
7	6	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 |-
8	7	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 |-
9	8	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 |-
10		ovex	$$⊢{ℝ}^{\left(1\dots 3\right)}\in \mathrm{V}$$
11	10 10	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 |-
12	11	a1i	Could not format ( ph -> ( 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 |- ( ph -> ( 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 |-
13	4 9 1 12	fvmptd3	Could not format ( ph -> ( 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 |- ( ph -> ( 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		oveq12	Could not format ( ( w = B /\ z = C ) -> ( w crossp z ) = ( B crossp C ) ) : No typesetting found for |- ( ( w = B /\ z = C ) -> ( w crossp z ) = ( B crossp C ) ) with typecode |-
15	14	fveq1d	Could not format ( ( w = B /\ z = C ) -> ( ( w crossp z ) ` k ) = ( ( B crossp C ) ` k ) ) : No typesetting found for |- ( ( w = B /\ z = C ) -> ( ( w crossp z ) ` k ) = ( ( B crossp C ) ` k ) ) with typecode |-
16	15	oveq2d	Could not format ( ( w = B /\ z = C ) -> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) : No typesetting found for |- ( ( w = B /\ z = C ) -> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) with typecode |-
17	16	mpteq2dv	Could not format ( ( 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 |- ( ( 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 |-
18	17	oveq2d	Could not format ( ( 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 |- ( ( 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 |-
19	18	adantl	Could not format ( ( ph /\ ( 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 |- ( ( ph /\ ( 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 |-
20		ovexd	Could not format ( ph -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) e. _V ) : No typesetting found for |- ( ph -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) e. _V ) with typecode |-
21	13 19 2 3 20	ovmpod	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 |-