Metamath Proof Explorer

Theorem crosspdotsumi

Description: Expand the group sum over ( 1 ... 3 ) into an explicit three-term sum. (A helper for crosspdoti .) (Contributed by Jiamin Zhao, 1-Aug-2026)

Ref Expression
Hypotheses crosspdotsumi.1 
|- A e. ( RR ^m ( 1 ... 3 ) )
crosspdotsumi.2 
|- B e. ( RR ^m ( 1 ... 3 ) )
crosspdotsumi.3 
|- C e. ( RR ^m ( 1 ... 3 ) )
Assertion crosspdotsumi 
|- ( 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 crosspdotsumi.1 
 |-  A e. ( RR ^m ( 1 ... 3 ) )
2 crosspdotsumi.2 
 |-  B e. ( RR ^m ( 1 ... 3 ) )
3 crosspdotsumi.3 
 |-  C e. ( RR ^m ( 1 ... 3 ) )
4 df-refld 
 |-  RRfld = ( CCfld |`s RR )
5 4 oveq1i 
 |-  ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( CCfld |`s RR ) gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) )
6 fzfid 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( 1 ... 3 ) e. Fin )
7 elmapi 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> A : ( 1 ... 3 ) --> RR )
8 7 ffvelcdmda 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ k e. ( 1 ... 3 ) ) -> ( A ` k ) e. RR )
9 2 3 crosspcli 
 |-  ( B crossp C ) e. ( RR ^m ( 1 ... 3 ) )
10 elmapi 
 |-  ( ( B crossp C ) e. ( RR ^m ( 1 ... 3 ) ) -> ( B crossp C ) : ( 1 ... 3 ) --> RR )
11 9 10 ax-mp 
 |-  ( B crossp C ) : ( 1 ... 3 ) --> RR
12 11 a1i 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ k e. ( 1 ... 3 ) ) -> ( B crossp C ) : ( 1 ... 3 ) --> RR )
13 simpr 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ k e. ( 1 ... 3 ) ) -> k e. ( 1 ... 3 ) )
14 12 13 ffvelcdmd 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ k e. ( 1 ... 3 ) ) -> ( ( B crossp C ) ` k ) e. RR )
15 8 14 remulcld 
 |-  ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ k e. ( 1 ... 3 ) ) -> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) e. RR )
16 6 15 regsumfsum 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( CCfld |`s RR ) gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = sum_ k e. ( 1 ... 3 ) ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) )
17 1 16 ax-mp 
 |-  ( ( CCfld |`s RR ) gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = sum_ k e. ( 1 ... 3 ) ( ( A ` k ) x. ( ( B crossp C ) ` k ) )
18 1p2e3 
 |-  ( 1 + 2 ) = 3
19 18 eqcomi 
 |-  3 = ( 1 + 2 )
20 19 oveq2i 
 |-  ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
21 1z 
 |-  1 e. ZZ
22 fztp 
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
23 21 22 ax-mp 
 |-  ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
24 20 23 eqtri 
 |-  ( 1 ... 3 ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
25 24 sumeq1i 
 |-  sum_ k e. ( 1 ... 3 ) ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) = sum_ k e. { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ( ( A ` k ) x. ( ( B crossp C ) ` k ) )
26 eqidd 
 |-  ( 1 e. ZZ -> 1 = 1 )
27 1p1e2 
 |-  ( 1 + 1 ) = 2
28 27 a1i 
 |-  ( 1 e. ZZ -> ( 1 + 1 ) = 2 )
29 18 a1i 
 |-  ( 1 e. ZZ -> ( 1 + 2 ) = 3 )
30 26 28 29 tpeq123d 
 |-  ( 1 e. ZZ -> { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
31 21 30 ax-mp 
 |-  { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 }
32 31 sumeq1i 
 |-  sum_ k e. { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) = sum_ k e. { 1 , 2 , 3 } ( ( A ` k ) x. ( ( B crossp C ) ` k ) )
33 fveq2 
 |-  ( k = 1 -> ( A ` k ) = ( A ` 1 ) )
34 fveq2 
 |-  ( k = 1 -> ( ( B crossp C ) ` k ) = ( ( B crossp C ) ` 1 ) )
35 33 34 oveq12d 
 |-  ( k = 1 -> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) = ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) )
36 fveq2 
 |-  ( k = 2 -> ( A ` k ) = ( A ` 2 ) )
37 fveq2 
 |-  ( k = 2 -> ( ( B crossp C ) ` k ) = ( ( B crossp C ) ` 2 ) )
38 36 37 oveq12d 
 |-  ( k = 2 -> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) = ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) )
39 fveq2 
 |-  ( k = 3 -> ( A ` k ) = ( A ` 3 ) )
40 fveq2 
 |-  ( k = 3 -> ( ( B crossp C ) ` k ) = ( ( B crossp C ) ` 3 ) )
41 39 40 oveq12d 
 |-  ( k = 3 -> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) = ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) )
42 1 rr3fv1cli 
 |-  ( A ` 1 ) e. RR
43 9 rr3fv1cli 
 |-  ( ( B crossp C ) ` 1 ) e. RR
44 42 43 remulcli 
 |-  ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) e. RR
45 44 recni 
 |-  ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) e. CC
46 45 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) e. CC )
47 1 rr3fv2cli 
 |-  ( A ` 2 ) e. RR
48 9 rr3fv2cli 
 |-  ( ( B crossp C ) ` 2 ) e. RR
49 47 48 remulcli 
 |-  ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) e. RR
50 49 recni 
 |-  ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) e. CC
51 50 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) e. CC )
52 1 rr3fv3cli 
 |-  ( A ` 3 ) e. RR
53 9 rr3fv3cli 
 |-  ( ( B crossp C ) ` 3 ) e. RR
54 52 53 remulcli 
 |-  ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) e. RR
55 54 recni 
 |-  ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) e. CC
56 55 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) e. CC )
57 46 51 56 3jca 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) e. CC /\ ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) e. CC /\ ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) e. CC ) )
58 2z 
 |-  2 e. ZZ
59 3z 
 |-  3 e. ZZ
60 21 58 59 3pm3.2i 
 |-  ( 1 e. ZZ /\ 2 e. ZZ /\ 3 e. ZZ )
61 60 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( 1 e. ZZ /\ 2 e. ZZ /\ 3 e. ZZ ) )
62 1ne2 
 |-  1 =/= 2
63 62 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> 1 =/= 2 )
64 1ne3 
 |-  1 =/= 3
65 64 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> 1 =/= 3 )
66 2ne3 
 |-  2 =/= 3
67 66 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> 2 =/= 3 )
68 35 38 41 57 61 63 65 67 sumtp 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> sum_ k e. { 1 , 2 , 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 ) ) ) )
69 1 68 ax-mp 
 |-  sum_ k e. { 1 , 2 , 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 ) ) )
70 45 50 55 addassi 
 |-  ( ( ( ( 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 crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) )
71 69 70 eqtri 
 |-  sum_ k e. { 1 , 2 , 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 ) ) ) )
72 25 32 71 3eqtri 
 |-  sum_ 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 ) ) ) )
73 5 17 72 3eqtri 
 |-  ( 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 ) ) ) )