Theorem crosspalti

Description: Antisymmetry of the cross product: swapping the two vectors negates the result. (Contributed by Jiamin Zhao, 1-Aug-2026)

	Ref	Expression
Hypotheses	crosspalti.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspalti.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspalti	Could not format assertion : No typesetting found for |- ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		crosspalti.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspalti.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3	1 2	crosspcli	Could not format ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) : No typesetting found for |- ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) with typecode |-
4		elmapfn	Could not format ( ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) Fn ( 1 ... 3 ) ) : No typesetting found for |- ( ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) Fn ( 1 ... 3 ) ) with typecode |-
5	3 4	ax-mp	Could not format ( A crossp B ) Fn ( 1 ... 3 ) : No typesetting found for |- ( A crossp B ) Fn ( 1 ... 3 ) with typecode |-
6	5	a1i	Could not format ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) Fn ( 1 ... 3 ) ) : No typesetting found for |- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) Fn ( 1 ... 3 ) ) with typecode |-
7		negex	Could not format -u ( ( B crossp A ) ` k ) e. _V : No typesetting found for |- -u ( ( B crossp A ) ` k ) e. _V with typecode |-
8		eqid	Could not format ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) : No typesetting found for |- ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) with typecode |-
9	7 8	fnmpti	Could not format ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) Fn ( 1 ... 3 ) : No typesetting found for |- ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) Fn ( 1 ... 3 ) with typecode |-
10	9	a1i	Could not format ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) Fn ( 1 ... 3 ) ) : No typesetting found for |- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) Fn ( 1 ... 3 ) ) with typecode |-
11		simpr	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to t=1$$
12	11	fveq2d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 1 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 1 ) ) with typecode |-
13	1 2	crosspv1i	Could not format ( ( A crossp B ) ` 1 ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) : No typesetting found for |- ( ( A crossp B ) ` 1 ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) with typecode |-
14	12 13	eqtrdi	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) ) with typecode |-
15	1	rr3fv2cli	$$⊢A\left(2\right)\in ℝ$$
16	15	recni	$$⊢A\left(2\right)\in ℂ$$
17	2	rr3fv3cli	$$⊢B\left(3\right)\in ℝ$$
18	17	recni	$$⊢B\left(3\right)\in ℂ$$
19	16 18	mulcomi	$$⊢A\left(2\right)B\left(3\right)=B\left(3\right)A\left(2\right)$$
20	19	a1i	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to A\left(2\right)B\left(3\right)=B\left(3\right)A\left(2\right)$$
21	1	rr3fv3cli	$$⊢A\left(3\right)\in ℝ$$
22	21	recni	$$⊢A\left(3\right)\in ℂ$$
23	2	rr3fv2cli	$$⊢B\left(2\right)\in ℝ$$
24	23	recni	$$⊢B\left(2\right)\in ℂ$$
25	22 24	mulcomi	$$⊢A\left(3\right)B\left(2\right)=B\left(2\right)A\left(3\right)$$
26	25	a1i	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to A\left(3\right)B\left(2\right)=B\left(2\right)A\left(3\right)$$
27	20 26	oveq12d	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)=B\left(3\right)A\left(2\right)-B\left(2\right)A\left(3\right)$$
28	23 21	remulcli	$$⊢B\left(2\right)A\left(3\right)\in ℝ$$
29	28	recni	$$⊢B\left(2\right)A\left(3\right)\in ℂ$$
30	17 15	remulcli	$$⊢B\left(3\right)A\left(2\right)\in ℝ$$
31	30	recni	$$⊢B\left(3\right)A\left(2\right)\in ℂ$$
32	29 31	negsubdi2i	$$⊢-\left(B\left(2\right)A\left(3\right)-B\left(3\right)A\left(2\right)\right)=B\left(3\right)A\left(2\right)-B\left(2\right)A\left(3\right)$$
33	27 32	eqtr4di	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)=-\left(B\left(2\right)A\left(3\right)-B\left(3\right)A\left(2\right)\right)$$
34	11	fveq2d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 1 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 1 ) ) with typecode |-
35	2 1	crosspv1i	Could not format ( ( B crossp A ) ` 1 ) = ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) : No typesetting found for |- ( ( B crossp A ) ` 1 ) = ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) with typecode |-
36	34 35	eqtrdi	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( B crossp A ) ` t ) = ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( B crossp A ) ` t ) = ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) ) with typecode |-
37	36	negeqd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> -u ( ( B crossp A ) ` t ) = -u ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> -u ( ( B crossp A ) ` t ) = -u ( ( ( B ` 2 ) x. ( A ` 3 ) ) - ( ( B ` 3 ) x. ( A ` 2 ) ) ) ) with typecode |-
38	33 37	eqtr4d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
39	14 38	eqtrd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
40	2 1	crosspv2i	Could not format ( ( B crossp A ) ` 2 ) = ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) : No typesetting found for |- ( ( B crossp A ) ` 2 ) = ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) with typecode |-
41	40	a1i	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B crossp A ) ` 2 ) = ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B crossp A ) ` 2 ) = ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) ) with typecode |-
42	41	negeqd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = -u ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = -u ( ( ( B ` 3 ) x. ( A ` 1 ) ) - ( ( B ` 1 ) x. ( A ` 3 ) ) ) ) with typecode |-
43	1	rr3fv1cli	$$⊢A\left(1\right)\in ℝ$$
44	17 43	remulcli	$$⊢B\left(3\right)A\left(1\right)\in ℝ$$
45	44	recni	$$⊢B\left(3\right)A\left(1\right)\in ℂ$$
46	2	rr3fv1cli	$$⊢B\left(1\right)\in ℝ$$
47		remulcl	$$⊢\left(B\left(1\right)\in ℝ\wedge A\left(3\right)\in ℝ\right)\to B\left(1\right)A\left(3\right)\in ℝ$$
48	47	recnd	$$⊢\left(B\left(1\right)\in ℝ\wedge A\left(3\right)\in ℝ\right)\to B\left(1\right)A\left(3\right)\in ℂ$$
49	46 21 48	mp2an	$$⊢B\left(1\right)A\left(3\right)\in ℂ$$
50	45 49	negsubdi2i	$$⊢-\left(B\left(3\right)A\left(1\right)-B\left(1\right)A\left(3\right)\right)=B\left(1\right)A\left(3\right)-B\left(3\right)A\left(1\right)$$
51	46	recni	$$⊢B\left(1\right)\in ℂ$$
52	51 22	mulcomi	$$⊢B\left(1\right)A\left(3\right)=A\left(3\right)B\left(1\right)$$
53	52	a1i	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to B\left(1\right)A\left(3\right)=A\left(3\right)B\left(1\right)$$
54	43	recni	$$⊢A\left(1\right)\in ℂ$$
55	18 54	mulcomi	$$⊢B\left(3\right)A\left(1\right)=A\left(1\right)B\left(3\right)$$
56	55	a1i	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to B\left(3\right)A\left(1\right)=A\left(1\right)B\left(3\right)$$
57	53 56	oveq12d	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to B\left(1\right)A\left(3\right)-B\left(3\right)A\left(1\right)=A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)$$
58	50 57	eqtrid	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to -\left(B\left(3\right)A\left(1\right)-B\left(1\right)A\left(3\right)\right)=A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)$$
59	42 58	eqtrd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) ) with typecode |-
60	1 2	crosspv2i	Could not format ( ( A crossp B ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) : No typesetting found for |- ( ( A crossp B ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) with typecode |-
61	59 60	eqtr4di	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = ( ( A crossp B ) ` 2 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` 2 ) = ( ( A crossp B ) ` 2 ) ) with typecode |-
62		simpr	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to t=1+1$$
63		1p1e2	$$⊢1+1=2$$
64	62 63	eqtrdi	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to t=2$$
65	64	fveq2d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 2 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 2 ) ) with typecode |-
66	65	negeqd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` t ) = -u ( ( B crossp A ) ` 2 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> -u ( ( B crossp A ) ` t ) = -u ( ( B crossp A ) ` 2 ) ) with typecode |-
67	64	fveq2d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 2 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 2 ) ) with typecode |-
68	61 66 67	3eqtr4rd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
69	2 1	crosspv3i	Could not format ( ( B crossp A ) ` 3 ) = ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) : No typesetting found for |- ( ( B crossp A ) ` 3 ) = ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) with typecode |-
70	69	a1i	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B crossp A ) ` 3 ) = ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B crossp A ) ` 3 ) = ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) ) with typecode |-
71	70	negeqd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = -u ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = -u ( ( ( B ` 1 ) x. ( A ` 2 ) ) - ( ( B ` 2 ) x. ( A ` 1 ) ) ) ) with typecode |-
72	46 15	remulcli	$$⊢B\left(1\right)A\left(2\right)\in ℝ$$
73	72	recni	$$⊢B\left(1\right)A\left(2\right)\in ℂ$$
74		remulcl	$$⊢\left(B\left(2\right)\in ℝ\wedge A\left(1\right)\in ℝ\right)\to B\left(2\right)A\left(1\right)\in ℝ$$
75	74	recnd	$$⊢\left(B\left(2\right)\in ℝ\wedge A\left(1\right)\in ℝ\right)\to B\left(2\right)A\left(1\right)\in ℂ$$
76	23 43 75	mp2an	$$⊢B\left(2\right)A\left(1\right)\in ℂ$$
77	73 76	negsubdi2i	$$⊢-\left(B\left(1\right)A\left(2\right)-B\left(2\right)A\left(1\right)\right)=B\left(2\right)A\left(1\right)-B\left(1\right)A\left(2\right)$$
78	24 54	mulcomi	$$⊢B\left(2\right)A\left(1\right)=A\left(1\right)B\left(2\right)$$
79	78	a1i	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to B\left(2\right)A\left(1\right)=A\left(1\right)B\left(2\right)$$
80	51 16	mulcomi	$$⊢B\left(1\right)A\left(2\right)=A\left(2\right)B\left(1\right)$$
81	80	a1i	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to B\left(1\right)A\left(2\right)=A\left(2\right)B\left(1\right)$$
82	79 81	oveq12d	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to B\left(2\right)A\left(1\right)-B\left(1\right)A\left(2\right)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
83	77 82	eqtrid	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to -\left(B\left(1\right)A\left(2\right)-B\left(2\right)A\left(1\right)\right)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
84	71 83	eqtrd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) with typecode |-
85	1 2	crosspv3i	Could not format ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) : No typesetting found for |- ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) with typecode |-
86	84 85	eqtr4di	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = ( ( A crossp B ) ` 3 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` 3 ) = ( ( A crossp B ) ` 3 ) ) with typecode |-
87		simpr	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to t=1+2$$
88		1p2e3	$$⊢1+2=3$$
89	87 88	eqtrdi	$$⊢\left(\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to t=3$$
90	89	fveq2d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 3 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( B crossp A ) ` t ) = ( ( B crossp A ) ` 3 ) ) with typecode |-
91	90	negeqd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` t ) = -u ( ( B crossp A ) ` 3 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> -u ( ( B crossp A ) ` t ) = -u ( ( B crossp A ) ` 3 ) ) with typecode |-
92	89	fveq2d	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 3 ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( A crossp B ) ` t ) = ( ( A crossp B ) ` 3 ) ) with typecode |-
93	86 91 92	3eqtr4rd	Could not format ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
94		simpr	$$⊢\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to t\in \left(1\dots 3\right)$$
95	88	eqcomi	$$⊢3=1+2$$
96	95	oveq2i	$$⊢\left(1\dots 3\right)=\left(1\dots 1+2\right)$$
97		1z	$$⊢1\in \mathbb{Z}$$
98		fztp	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
99	97 98	ax-mp	$$⊢\left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
100	96 99	eqtri	$$⊢\left(1\dots 3\right)=\left\{1,1+1,1+2\right\}$$
101	94 100	eleqtrdi	$$⊢\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to t\in \left\{1,1+1,1+2\right\}$$
102		eltpi	$$⊢t\in \left\{1,1+1,1+2\right\}\to \left(t=1\vee t=1+1\vee t=1+2\right)$$
103	101 102	syl	$$⊢\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to \left(t=1\vee t=1+1\vee t=1+2\right)$$
104	39 68 93 103	mpjao3dan	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( A crossp B ) ` t ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
105		fveq2	Could not format ( k = t -> ( ( B crossp A ) ` k ) = ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( k = t -> ( ( B crossp A ) ` k ) = ( ( B crossp A ) ` t ) ) with typecode |-
106	105	negeqd	Could not format ( k = t -> -u ( ( B crossp A ) ` k ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( k = t -> -u ( ( B crossp A ) ` k ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
107		negex	Could not format -u ( ( B crossp A ) ` t ) e. _V : No typesetting found for |- -u ( ( B crossp A ) ` t ) e. _V with typecode |-
108	107	a1i	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> -u ( ( B crossp A ) ` t ) e. _V ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> -u ( ( B crossp A ) ` t ) e. _V ) with typecode |-
109	8 106 94 108	fvmptd3	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ` t ) = -u ( ( B crossp A ) ` t ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ` t ) = -u ( ( B crossp A ) ` t ) ) with typecode |-
110	104 109	eqtr4d	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( A crossp B ) ` t ) = ( ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ` t ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( A crossp B ) ` t ) = ( ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ` t ) ) with typecode |-
111	6 10 110	eqfnfvd	Could not format ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ) : No typesetting found for |- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) ) with typecode |-
112	1 111	ax-mp	Could not format ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) : No typesetting found for |- ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> -u ( ( B crossp A ) ` k ) ) with typecode |-