Metamath Proof Explorer

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 
|- ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
crosspdot0lem.2 
|- ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
crosspdot0lem.3 
|- ( ph -> C e. ( RR ^m ( 1 ... 3 ) ) )
Assertion crosspdot0lem 
|- ( ph -> ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 crosspdot0lem.1 
 |-  ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
2 crosspdot0lem.2 
 |-  ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
3 crosspdot0lem.3 
 |-  ( ph -> C e. ( RR ^m ( 1 ... 3 ) ) )
4 df-tripp 
 |-  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 ) ) ) ) ) )
5 fveq1 
 |-  ( s = A -> ( s ` k ) = ( A ` k ) )
6 5 oveq1d 
 |-  ( s = A -> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) )
7 6 mpteq2dv 
 |-  ( s = A -> ( k e. ( 1 ... 3 ) |-> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) ) = ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) ) )
8 7 oveq2d 
 |-  ( 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 ) ) ) ) )
9 8 mpoeq3dv 
 |-  ( 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 ) ) ) ) ) )
10 ovex 
 |-  ( RR ^m ( 1 ... 3 ) ) e. _V
11 10 10 mpoex 
 |-  ( 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
12 11 a1i 
 |-  ( 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 )
13 4 9 1 12 fvmptd3 
 |-  ( 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 ) ) ) ) ) )
14 oveq12 
 |-  ( ( w = B /\ z = C ) -> ( w crossp z ) = ( B crossp C ) )
15 14 fveq1d 
 |-  ( ( w = B /\ z = C ) -> ( ( w crossp z ) ` k ) = ( ( B crossp C ) ` k ) )
16 15 oveq2d 
 |-  ( ( w = B /\ z = C ) -> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) )
17 16 mpteq2dv 
 |-  ( ( 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 ) ) ) )
18 17 oveq2d 
 |-  ( ( 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 ) ) ) ) )
19 18 adantl 
 |-  ( ( 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 ) ) ) ) )
20 ovexd 
 |-  ( ph -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) e. _V )
21 13 19 2 3 20 ovmpod 
 |-  ( ph -> ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) )