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\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdotsumi.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspdotsumi.3	$$⊢C\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspdotsumi	Could not format assertion : No typesetting found for |- ( 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 ) ) ) ) with typecode |-

Proof

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