Metamath Proof Explorer

Theorem crosspdotsumlem

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

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