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

Proof

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