Theorem crosspaltd

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

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

Proof

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