Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 crosspdot0i.1 
 |-  A e. ( RR ^m ( 1 ... 3 ) )
2 crosspdot0i.2 
 |-  B e. ( RR ^m ( 1 ... 3 ) )
3 crosspdot0i.3 
 |-  C e. ( RR ^m ( 1 ... 3 ) )
4 ovex 
 |-  ( RR ^m ( 1 ... 3 ) ) e. _V
5 4 4 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
6 fveq1 
 |-  ( s = A -> ( s ` k ) = ( A ` k ) )
7 6 oveq1d 
 |-  ( s = A -> ( ( s ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) )
8 7 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 ) ) ) )
9 8 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 ) ) ) ) )
10 9 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 ) ) ) ) ) )
11 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 ) ) ) ) ) )
12 10 11 fvmptg 
 |-  ( ( 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 ) ) ) ) ) )
13 1 5 12 mp2an 
 |-  ( 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 13 oveqi 
 |-  ( 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 )
15 eqidd 
 |-  ( 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 ) ) ) ) ) )
16 simprl 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> w = B )
17 simprr 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> z = C )
18 16 17 oveq12d 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( w crossp z ) = ( B crossp C ) )
19 18 fveq1d 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( ( w crossp z ) ` k ) = ( ( B crossp C ) ` k ) )
20 19 oveq2d 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ ( w = B /\ z = C ) ) -> ( ( A ` k ) x. ( ( w crossp z ) ` k ) ) = ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) )
21 20 mpteq2dv 
 |-  ( ( 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 ) ) ) )
22 21 oveq2d 
 |-  ( ( 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 ) ) ) ) )
23 2 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> B e. ( RR ^m ( 1 ... 3 ) ) )
24 3 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> C e. ( RR ^m ( 1 ... 3 ) ) )
25 ovexd 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) e. _V )
26 15 22 23 24 25 ovmpod 
 |-  ( 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 ) ) ) ) )
27 1 26 ax-mp 
 |-  ( 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 ) ) ) )
28 14 27 eqtri 
 |-  ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) )