Theorem crossp3i

Description: The vector triple product expansion (BAC-CAB rule): the cross product of X with ( Y crossp Z ) equals Y scaled by the dot product of X and Z , minus Z scaled by the dot product of X and Y . The dot products are written out as explicit three-term sums of component products, matching the pointwise style of df-crossp rather than introducing a separate dot product operator. (Contributed by Jiamin Zhao, 1-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		crossp3i.1	$$⊢X\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crossp3i.2	$$⊢Y\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		crossp3i.3	$$⊢Z\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
4	2 3	crosspcli	Could not format ( Y crossp Z ) e. ( RR ^m ( 1 ... 3 ) ) : No typesetting found for |- ( Y crossp Z ) e. ( RR ^m ( 1 ... 3 ) ) with typecode |-
5	1 4	crosspcli	Could not format ( X crossp ( Y crossp Z ) ) e. ( RR ^m ( 1 ... 3 ) ) : No typesetting found for |- ( X crossp ( Y crossp Z ) ) e. ( RR ^m ( 1 ... 3 ) ) with typecode |-
6		elmapi	Could not format ( ( X crossp ( Y crossp Z ) ) e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR ) : No typesetting found for |- ( ( X crossp ( Y crossp Z ) ) e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR ) with typecode |-
7	5 6	ax-mp	Could not format ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR : No typesetting found for |- ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR with typecode |-
8		ffn	Could not format ( ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR -> ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) ) : No typesetting found for |- ( ( X crossp ( Y crossp Z ) ) : ( 1 ... 3 ) --> RR -> ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) ) with typecode |-
9	7 8	ax-mp	Could not format ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) : No typesetting found for |- ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) with typecode |-
10	9	a1i	Could not format ( X e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) ) : No typesetting found for |- ( X e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) Fn ( 1 ... 3 ) ) with typecode |-
11		eqid	$$⊢\left(k\in \left(1\dots 3\right)⟼\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\right)=\left(k\in \left(1\dots 3\right)⟼\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\right)$$
12	11	fnmpt	$$⊢\forall k\in \left(1\dots 3\right)\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\in ℝ\to \left(k\in \left(1\dots 3\right)⟼\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\right)Fn\left(1\dots 3\right)$$
13	1	rr3fv1cli	$$⊢X\left(1\right)\in ℝ$$
14	3	rr3fv1cli	$$⊢Z\left(1\right)\in ℝ$$
15	13 14	remulcli	$$⊢X\left(1\right)Z\left(1\right)\in ℝ$$
16	1	rr3fv2cli	$$⊢X\left(2\right)\in ℝ$$
17	3	rr3fv2cli	$$⊢Z\left(2\right)\in ℝ$$
18	16 17	remulcli	$$⊢X\left(2\right)Z\left(2\right)\in ℝ$$
19	15 18	readdcli	$$⊢X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\in ℝ$$
20	1	rr3fv3cli	$$⊢X\left(3\right)\in ℝ$$
21	3	rr3fv3cli	$$⊢Z\left(3\right)\in ℝ$$
22	20 21	remulcli	$$⊢X\left(3\right)Z\left(3\right)\in ℝ$$
23	19 22	readdcli	$$⊢X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\in ℝ$$
24	23	a1i	$$⊢k\in \left(1\dots 3\right)\to X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\in ℝ$$
25		elmapi	$$⊢Y\in \left({ℝ}^{\left(1\dots 3\right)}\right)\to Y:\left(1\dots 3\right)⟶ℝ$$
26	2 25	ax-mp	$$⊢Y:\left(1\dots 3\right)⟶ℝ$$
27	26	ffvelcdmi	$$⊢k\in \left(1\dots 3\right)\to Y\left(k\right)\in ℝ$$
28	24 27	remulcld	$$⊢k\in \left(1\dots 3\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)\in ℝ$$
29	2	rr3fv1cli	$$⊢Y\left(1\right)\in ℝ$$
30	13 29	remulcli	$$⊢X\left(1\right)Y\left(1\right)\in ℝ$$
31	2	rr3fv2cli	$$⊢Y\left(2\right)\in ℝ$$
32	16 31	remulcli	$$⊢X\left(2\right)Y\left(2\right)\in ℝ$$
33	30 32	readdcli	$$⊢X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\in ℝ$$
34	2	rr3fv3cli	$$⊢Y\left(3\right)\in ℝ$$
35	20 34	remulcli	$$⊢X\left(3\right)Y\left(3\right)\in ℝ$$
36	33 35	readdcli	$$⊢X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\in ℝ$$
37	36	a1i	$$⊢k\in \left(1\dots 3\right)\to X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\in ℝ$$
38		elmapi	$$⊢Z\in \left({ℝ}^{\left(1\dots 3\right)}\right)\to Z:\left(1\dots 3\right)⟶ℝ$$
39	3 38	ax-mp	$$⊢Z:\left(1\dots 3\right)⟶ℝ$$
40	39	ffvelcdmi	$$⊢k\in \left(1\dots 3\right)\to Z\left(k\right)\in ℝ$$
41	37 40	remulcld	$$⊢k\in \left(1\dots 3\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\in ℝ$$
42	28 41	resubcld	$$⊢k\in \left(1\dots 3\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\in ℝ$$
43	12 42	mprg	$$⊢\left(k\in \left(1\dots 3\right)⟼\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\right)Fn\left(1\dots 3\right)$$
44	43	a1i	$$⊢X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\to \left(k\in \left(1\dots 3\right)⟼\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\right)Fn\left(1\dots 3\right)$$
45		simpr	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to t=1$$
46	45	fveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` 1 ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` 1 ) ) with typecode |-
47	1 4	crosspv1i	Could not format ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) : No typesetting found for |- ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) with typecode |-
48	2 3	crosspv3i	Could not format ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) : No typesetting found for |- ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) with typecode |-
49	48	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) with typecode |-
50	49	oveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) = ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) = ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) with typecode |-
51	2 3	crosspv2i	Could not format ( ( Y crossp Z ) ` 2 ) = ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) : No typesetting found for |- ( ( Y crossp Z ) ` 2 ) = ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) with typecode |-
52	51	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y crossp Z ) ` 2 ) = ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( Y crossp Z ) ` 2 ) = ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) with typecode |-
53	52	oveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) = ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) = ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) with typecode |-
54	50 53	oveq12d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 3 ) ) - ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) ) with typecode |-
55	47 54	eqtrid	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( X ` 2 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) - ( ( X ` 3 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) ) ) with typecode |-
56	16	recni	$$⊢X\left(2\right)\in ℂ$$
57	56	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)\in ℂ$$
58	29 17	remulcli	$$⊢Y\left(1\right)Z\left(2\right)\in ℝ$$
59	58	recni	$$⊢Y\left(1\right)Z\left(2\right)\in ℂ$$
60	59	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(1\right)Z\left(2\right)\in ℂ$$
61	31 14	remulcli	$$⊢Y\left(2\right)Z\left(1\right)\in ℝ$$
62	61	recni	$$⊢Y\left(2\right)Z\left(1\right)\in ℂ$$
63	62	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(2\right)Z\left(1\right)\in ℂ$$
64	57 60 63	subdid	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)\left(Y\left(1\right)Z\left(2\right)-Y\left(2\right)Z\left(1\right)\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)$$
65	20	recni	$$⊢X\left(3\right)\in ℂ$$
66	65	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)\in ℂ$$
67	34 14	remulcli	$$⊢Y\left(3\right)Z\left(1\right)\in ℝ$$
68	67	recni	$$⊢Y\left(3\right)Z\left(1\right)\in ℂ$$
69	68	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(3\right)Z\left(1\right)\in ℂ$$
70	29 21	remulcli	$$⊢Y\left(1\right)Z\left(3\right)\in ℝ$$
71	70	recni	$$⊢Y\left(1\right)Z\left(3\right)\in ℂ$$
72	71	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(1\right)Z\left(3\right)\in ℂ$$
73	66 69 72	subdid	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)\left(Y\left(3\right)Z\left(1\right)-Y\left(1\right)Z\left(3\right)\right)=X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)$$
74	64 73	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)\left(Y\left(1\right)Z\left(2\right)-Y\left(2\right)Z\left(1\right)\right)-X\left(3\right)\left(Y\left(3\right)Z\left(1\right)-Y\left(1\right)Z\left(3\right)\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)$$
75	13	recni	$$⊢X\left(1\right)\in ℂ$$
76	14	recni	$$⊢Z\left(1\right)\in ℂ$$
77	75 76	mulcli	$$⊢X\left(1\right)Z\left(1\right)\in ℂ$$
78	17	recni	$$⊢Z\left(2\right)\in ℂ$$
79	56 78	mulcli	$$⊢X\left(2\right)Z\left(2\right)\in ℂ$$
80	77 79	addcli	$$⊢X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\in ℂ$$
81	80	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\in ℂ$$
82	21	recni	$$⊢Z\left(3\right)\in ℂ$$
83	65 82	mulcli	$$⊢X\left(3\right)Z\left(3\right)\in ℂ$$
84	83	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Z\left(3\right)\in ℂ$$
85	29	recni	$$⊢Y\left(1\right)\in ℂ$$
86	85	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(1\right)\in ℂ$$
87	81 84 86	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(1\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)$$
88	75 85	mulcli	$$⊢X\left(1\right)Y\left(1\right)\in ℂ$$
89	31	recni	$$⊢Y\left(2\right)\in ℂ$$
90	56 89	mulcli	$$⊢X\left(2\right)Y\left(2\right)\in ℂ$$
91	88 90	addcli	$$⊢X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\in ℂ$$
92	91	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\in ℂ$$
93	34	recni	$$⊢Y\left(3\right)\in ℂ$$
94	65 93	mulcli	$$⊢X\left(3\right)Y\left(3\right)\in ℂ$$
95	94	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Y\left(3\right)\in ℂ$$
96	76	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(1\right)\in ℂ$$
97	92 95 96	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(1\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)+X\left(3\right)Y\left(3\right)Z\left(1\right)$$
98	87 97	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(1\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)+X\left(3\right)Y\left(3\right)Z\left(1\right)\right)$$
99	80 85	mulcli	$$⊢\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)\in ℂ$$
100	99	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)\in ℂ$$
101	83 85	mulcli	$$⊢X\left(3\right)Z\left(3\right)Y\left(1\right)\in ℂ$$
102	101	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Z\left(3\right)Y\left(1\right)\in ℂ$$
103	91 76	mulcli	$$⊢\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)\in ℂ$$
104	103	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)\in ℂ$$
105	94 76	mulcli	$$⊢X\left(3\right)Y\left(3\right)Z\left(1\right)\in ℂ$$
106	105	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Y\left(3\right)Z\left(1\right)\in ℂ$$
107	100 102 104 106	addsub4d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)+X\left(3\right)Y\left(3\right)Z\left(1\right)\right)=\left(\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
108	77	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)\in ℂ$$
109	79	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Z\left(2\right)\in ℂ$$
110	108 109 86	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)=X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)$$
111	88	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)\in ℂ$$
112	90	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Y\left(2\right)\in ℂ$$
113	111 112 96	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)$$
114	110 113	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)=X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)$$
115	114	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=\left(X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
116	75	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)\in ℂ$$
117	116 96 86	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)Y\left(1\right)=X\left(1\right)Z\left(1\right)Y\left(1\right)$$
118	96 86	mulcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(1\right)Y\left(1\right)=Y\left(1\right)Z\left(1\right)$$
119	118	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)Y\left(1\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)$$
120	117 119	eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)Y\left(1\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)$$
121	120	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)$$
122	121	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)$$
123	122	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
124	116 86 96	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)Z\left(1\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)$$
125	124	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)$$
126	125	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)=X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)$$
127	126	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
128	85 76	mulcli	$$⊢Y\left(1\right)Z\left(1\right)\in ℂ$$
129	75 128	mulcli	$$⊢X\left(1\right)Y\left(1\right)Z\left(1\right)\in ℂ$$
130	129	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)Z\left(1\right)\in ℂ$$
131	79 85	mulcli	$$⊢X\left(2\right)Z\left(2\right)Y\left(1\right)\in ℂ$$
132	131	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Z\left(2\right)Y\left(1\right)\in ℂ$$
133	90 76	mulcli	$$⊢X\left(2\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
134	133	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
135	130 132 134	pnpcand	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)=X\left(2\right)Z\left(2\right)Y\left(1\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)$$
136	135	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=\left(X\left(2\right)Z\left(2\right)Y\left(1\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
137	78	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(2\right)\in ℂ$$
138	57 137 86	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Z\left(2\right)Y\left(1\right)=X\left(2\right)Z\left(2\right)Y\left(1\right)$$
139	137 86	mulcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(2\right)Y\left(1\right)=Y\left(1\right)Z\left(2\right)$$
140	139	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Z\left(2\right)Y\left(1\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)$$
141	138 140	eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Z\left(2\right)Y\left(1\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)$$
142	89	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(2\right)\in ℂ$$
143	57 142 96	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Y\left(2\right)Z\left(1\right)=X\left(2\right)Y\left(2\right)Z\left(1\right)$$
144	141 143	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Z\left(2\right)Y\left(1\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)$$
145	82	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(3\right)\in ℂ$$
146	66 145 86	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Z\left(3\right)Y\left(1\right)=X\left(3\right)Z\left(3\right)Y\left(1\right)$$
147	145 86	mulcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(3\right)Y\left(1\right)=Y\left(1\right)Z\left(3\right)$$
148	147	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Z\left(3\right)Y\left(1\right)=X\left(3\right)Y\left(1\right)Z\left(3\right)$$
149	146 148	eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Z\left(3\right)Y\left(1\right)=X\left(3\right)Y\left(1\right)Z\left(3\right)$$
150	93	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(3\right)\in ℂ$$
151	66 150 96	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Y\left(3\right)Z\left(1\right)=X\left(3\right)Y\left(3\right)Z\left(1\right)$$
152	149 151	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=X\left(3\right)Y\left(1\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
153	144 152	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(2\right)Z\left(2\right)Y\left(1\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=\left(X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Y\left(1\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
154	85 78	mulcli	$$⊢Y\left(1\right)Z\left(2\right)\in ℂ$$
155	56 154	mulcli	$$⊢X\left(2\right)Y\left(1\right)Z\left(2\right)\in ℂ$$
156	89 76	mulcli	$$⊢Y\left(2\right)Z\left(1\right)\in ℂ$$
157	56 156	mulcli	$$⊢X\left(2\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
158	155 157	subcli	$$⊢X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
159	158	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
160	93 76	mulcli	$$⊢Y\left(3\right)Z\left(1\right)\in ℂ$$
161	65 160	mulcli	$$⊢X\left(3\right)Y\left(3\right)Z\left(1\right)\in ℂ$$
162	161	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Y\left(3\right)Z\left(1\right)\in ℂ$$
163	85 82	mulcli	$$⊢Y\left(1\right)Z\left(3\right)\in ℂ$$
164	65 163	mulcli	$$⊢X\left(3\right)Y\left(1\right)Z\left(3\right)\in ℂ$$
165	164	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(3\right)Y\left(1\right)Z\left(3\right)\in ℂ$$
166	159 162 165	subsub2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)=\left(X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Y\left(1\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)$$
167	153 166	eqtr4d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(2\right)Z\left(2\right)Y\left(1\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)$$
168	136 167	eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)$$
169	123 127 168	3eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)Y\left(1\right)+X\left(2\right)Z\left(2\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(1\right)\right)\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-X\left(3\right)Y\left(3\right)Z\left(1\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)$$
170	107 115 169	3eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(1\right)+X\left(3\right)Z\left(3\right)Y\left(1\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(1\right)+X\left(3\right)Y\left(3\right)Z\left(1\right)\right)=X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)$$
171	98 170	eqtr2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to X\left(2\right)Y\left(1\right)Z\left(2\right)-X\left(2\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(1\right)-X\left(3\right)Y\left(1\right)Z\left(3\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(1\right)$$
172	55 74 171	3eqtrd	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` 1 ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 1 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 1 ) ) ) ) with typecode |-
173	45	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to 1=t$$
174	173	fveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Y\left(1\right)=Y\left(t\right)$$
175	174	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(1\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)$$
176	173	fveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to Z\left(1\right)=Z\left(t\right)$$
177	176	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(1\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
178	175 177	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(1\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(1\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
179	46 172 178	3eqtrd	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = 1 ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) with typecode |-
180		simpr	$$⊢\left(\left(X\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$$
181		1p1e2	$$⊢1+1=2$$
182	180 181	eqtrdi	$$⊢\left(\left(X\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$$
183	182	fveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` 2 ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` 2 ) ) with typecode |-
184	1 4	crosspv2i	Could not format ( ( X crossp ( Y crossp Z ) ) ` 2 ) = ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) : No typesetting found for |- ( ( X crossp ( Y crossp Z ) ) ` 2 ) = ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) with typecode |-
185	184	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 2 ) = ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 2 ) = ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) ) with typecode |-
186	2 3	crosspv1i	Could not format ( ( Y crossp Z ) ` 1 ) = ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) : No typesetting found for |- ( ( Y crossp Z ) ` 1 ) = ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) with typecode |-
187	186	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y crossp Z ) ` 1 ) = ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y crossp Z ) ` 1 ) = ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) with typecode |-
188	187	oveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) = ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) = ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) with typecode |-
189	48	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( Y crossp Z ) ` 3 ) = ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) with typecode |-
190	189	oveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) = ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) = ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) with typecode |-
191	188 190	oveq12d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( X ` 3 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) - ( ( X ` 1 ) x. ( ( ( Y ` 1 ) x. ( Z ` 2 ) ) - ( ( Y ` 2 ) x. ( Z ` 1 ) ) ) ) ) ) with typecode |-
192	65	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)\in ℂ$$
193	89 82	mulcli	$$⊢Y\left(2\right)Z\left(3\right)\in ℂ$$
194	193	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(2\right)Z\left(3\right)\in ℂ$$
195	93 78	mulcli	$$⊢Y\left(3\right)Z\left(2\right)\in ℂ$$
196	195	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(3\right)Z\left(2\right)\in ℂ$$
197	192 194 196	subdid	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)\left(Y\left(2\right)Z\left(3\right)-Y\left(3\right)Z\left(2\right)\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)$$
198	75	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)\in ℂ$$
199	154	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(1\right)Z\left(2\right)\in ℂ$$
200	156	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(2\right)Z\left(1\right)\in ℂ$$
201	198 199 200	subdid	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)\left(Y\left(1\right)Z\left(2\right)-Y\left(2\right)Z\left(1\right)\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)$$
202	197 201	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)\left(Y\left(2\right)Z\left(3\right)-Y\left(3\right)Z\left(2\right)\right)-X\left(1\right)\left(Y\left(1\right)Z\left(2\right)-Y\left(2\right)Z\left(1\right)\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)$$
203	75 156	mulcli	$$⊢X\left(1\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
204	203	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)\in ℂ$$
205	89 78	mulcli	$$⊢Y\left(2\right)Z\left(2\right)\in ℂ$$
206	56 205	mulcli	$$⊢X\left(2\right)Y\left(2\right)Z\left(2\right)\in ℂ$$
207	206	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)\in ℂ$$
208	204 207	addcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)$$
209	208	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)$$
210	75 154	mulcli	$$⊢X\left(1\right)Y\left(1\right)Z\left(2\right)\in ℂ$$
211	210	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)\in ℂ$$
212	211 207	addcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)$$
213	212	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
214	209 213	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=\left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
215	65 193	mulcli	$$⊢X\left(3\right)Y\left(2\right)Z\left(3\right)\in ℂ$$
216	215	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)\in ℂ$$
217	207 204 216	addassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)$$
218	65 195	mulcli	$$⊢X\left(3\right)Y\left(3\right)Z\left(2\right)\in ℂ$$
219	218	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(3\right)Z\left(2\right)\in ℂ$$
220	207 211 219	addassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
221	217 220	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)+\left(X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)\right)-\left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
222	203 215	addcli	$$⊢X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)\in ℂ$$
223	222	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)\in ℂ$$
224	210 218	addcli	$$⊢X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\in ℂ$$
225	224	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\in ℂ$$
226	207 223 225	pnpcand	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)+\left(X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)\right)-\left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
227	216 219 211 204	subadd4d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)\right)$$
228	216 204	addcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)=X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)$$
229	219 211	addcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(3\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
230	228 229	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)-\left(X\left(3\right)Y\left(3\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)\right)=X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
231	227 230	eqtr2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)$$
232	221 226 231	3eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(2\right)Z\left(1\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)$$
233	214 232	eqtr2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)=\left(X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
234	76	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Z\left(1\right)\in ℂ$$
235	89	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(2\right)\in ℂ$$
236	234 235	mulcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Z\left(1\right)Y\left(2\right)=Y\left(2\right)Z\left(1\right)$$
237	236	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)=X\left(1\right)Y\left(2\right)Z\left(1\right)$$
238	237	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)$$
239	78	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Z\left(2\right)\in ℂ$$
240	239 235	mulcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Z\left(2\right)Y\left(2\right)=Y\left(2\right)Z\left(2\right)$$
241	240	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Z\left(2\right)Y\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)$$
242	241	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(2\right)Z\left(2\right)Y\left(2\right)$$
243	238 242	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)$$
244	243	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)$$
245	244	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(2\right)Z\left(1\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=\left(X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
246	198 234 235	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)$$
247	246	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)$$
248	56	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)\in ℂ$$
249	248 239 235	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Z\left(2\right)Y\left(2\right)=X\left(2\right)Z\left(2\right)Y\left(2\right)$$
250	249	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Z\left(2\right)Y\left(2\right)=X\left(2\right)Z\left(2\right)Y\left(2\right)$$
251	247 250	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)$$
252	251	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)$$
253	85	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(1\right)\in ℂ$$
254	198 253 239	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)$$
255	254	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)$$
256	248 235 239	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)$$
257	256	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(2\right)Y\left(2\right)Z\left(2\right)$$
258	255 257	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)$$
259	258	oveq1d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
260	252 259	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=\left(X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
261	233 245 260	3eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)=\left(X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
262	77	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)\in ℂ$$
263	79	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Z\left(2\right)\in ℂ$$
264	262 263 235	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)=X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)$$
265	264	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)$$
266	65 82 89	mulassi	$$⊢X\left(3\right)Z\left(3\right)Y\left(2\right)=X\left(3\right)Z\left(3\right)Y\left(2\right)$$
267	82 89	mulcomi	$$⊢Z\left(3\right)Y\left(2\right)=Y\left(2\right)Z\left(3\right)$$
268	267	oveq2i	$$⊢X\left(3\right)Z\left(3\right)Y\left(2\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)$$
269	266 268	eqtri	$$⊢X\left(3\right)Z\left(3\right)Y\left(2\right)=X\left(3\right)Y\left(2\right)Z\left(3\right)$$
270	269	eqcomi	$$⊢X\left(3\right)Y\left(2\right)Z\left(3\right)=X\left(3\right)Z\left(3\right)Y\left(2\right)$$
271	270	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)=X\left(3\right)Z\left(3\right)Y\left(2\right)$$
272	265 271	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(2\right)$$
273	88	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)\in ℂ$$
274	90	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(2\right)Y\left(2\right)\in ℂ$$
275	273 274 239	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)$$
276	93	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(3\right)\in ℂ$$
277	192 276 239	mulassd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(3\right)Z\left(2\right)=X\left(3\right)Y\left(3\right)Z\left(2\right)$$
278	275 277	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)=X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
279	278	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
280	272 279	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)Y\left(2\right)+X\left(2\right)Z\left(2\right)Y\left(2\right)\right)+X\left(3\right)Y\left(2\right)Z\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)+X\left(2\right)Y\left(2\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(2\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)$$
281	80	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\in ℂ$$
282	83	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Z\left(3\right)\in ℂ$$
283	281 282 235	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(2\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(2\right)$$
284	283	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(2\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(2\right)$$
285	91	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\in ℂ$$
286	94	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(3\right)\in ℂ$$
287	285 286 239	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(2\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)$$
288	287	eqcomd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(2\right)$$
289	284 288	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(2\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(2\right)+X\left(3\right)Y\left(3\right)Z\left(2\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(2\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(2\right)$$
290	261 280 289	3eqtrd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to X\left(3\right)Y\left(2\right)Z\left(3\right)-X\left(3\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(2\right)-X\left(1\right)Y\left(2\right)Z\left(1\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(2\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(2\right)$$
291	191 202 290	3eqtrd	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` 2 ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` 2 ) ) ) ) with typecode |-
292	182	fveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Y\left(t\right)=Y\left(2\right)$$
293	292	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(2\right)$$
294	182	fveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to Z\left(t\right)=Z\left(2\right)$$
295	294	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(2\right)$$
296	293 295	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+1\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(2\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(2\right)$$
297	291 296	eqtr4d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( ( X ` 3 ) x. ( ( Y crossp Z ) ` 1 ) ) - ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 3 ) ) ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) with typecode |-
298	183 185 297	3eqtrd	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 1 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) with typecode |-
299		simpr	$$⊢\left(\left(X\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$$
300	299	fveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` ( 1 + 2 ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( X crossp ( Y crossp Z ) ) ` ( 1 + 2 ) ) ) with typecode |-
301		1p2e3	$$⊢1+2=3$$
302	301	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to 1+2=3$$
303	302	fveq2d	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` ( 1 + 2 ) ) = ( ( X crossp ( Y crossp Z ) ) ` 3 ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` ( 1 + 2 ) ) = ( ( X crossp ( Y crossp Z ) ) ` 3 ) ) with typecode |-
304	1 4	crosspv3i	Could not format ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) : No typesetting found for |- ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) with typecode |-
305	304	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) ) with typecode |-
306	51	oveq2i	Could not format ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) = ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) : No typesetting found for |- ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) = ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) with typecode |-
307	186	oveq2i	Could not format ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) = ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) : No typesetting found for |- ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) = ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) with typecode |-
308	306 307	oveq12i	Could not format ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) : No typesetting found for |- ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) with typecode |-
309	308	a1i	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( ( X ` 1 ) x. ( ( Y crossp Z ) ` 2 ) ) - ( ( X ` 2 ) x. ( ( Y crossp Z ) ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( ( ( Y ` 3 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 3 ) ) ) ) - ( ( X ` 2 ) x. ( ( ( Y ` 2 ) x. ( Z ` 3 ) ) - ( ( Y ` 3 ) x. ( Z ` 2 ) ) ) ) ) ) with typecode |-
310	75 160 163	subdii	$$⊢X\left(1\right)\left(Y\left(3\right)Z\left(1\right)-Y\left(1\right)Z\left(3\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)$$
311	56 193 195	subdii	$$⊢X\left(2\right)\left(Y\left(2\right)Z\left(3\right)-Y\left(3\right)Z\left(2\right)\right)=X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)$$
312	310 311	oveq12i	$$⊢X\left(1\right)\left(Y\left(3\right)Z\left(1\right)-Y\left(1\right)Z\left(3\right)\right)-X\left(2\right)\left(Y\left(2\right)Z\left(3\right)-Y\left(3\right)Z\left(2\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)$$
313	80	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\in ℂ$$
314	83	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(3\right)Z\left(3\right)\in ℂ$$
315	26	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Y:\left(1\dots 3\right)⟶ℝ$$
316		simplr	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to t\in \left(1\dots 3\right)$$
317	315 316	ffvelcdmd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Y\left(t\right)\in ℝ$$
318	317	recnd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Y\left(t\right)\in ℂ$$
319	313 314 318	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(t\right)+X\left(3\right)Z\left(3\right)Y\left(t\right)$$
320	91	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\in ℂ$$
321	94	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(3\right)Y\left(3\right)\in ℂ$$
322	39	a1i	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Z:\left(1\dots 3\right)⟶ℝ$$
323	322 316	ffvelcdmd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Z\left(t\right)\in ℝ$$
324	323	recnd	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Z\left(t\right)\in ℂ$$
325	320 321 324	adddird	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(t\right)+X\left(3\right)Y\left(3\right)Z\left(t\right)$$
326	319 325	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(t\right)+X\left(3\right)Z\left(3\right)Y\left(t\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(t\right)+X\left(3\right)Y\left(3\right)Z\left(t\right)\right)$$
327	299 301	eqtrdi	$$⊢\left(\left(X\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$$
328	327	fveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Y\left(t\right)=Y\left(3\right)$$
329	328	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)$$
330	328	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(3\right)Z\left(3\right)Y\left(t\right)=X\left(3\right)Z\left(3\right)Y\left(3\right)$$
331	329 330	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(t\right)+X\left(3\right)Z\left(3\right)Y\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)$$
332	327	fveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to Z\left(t\right)=Z\left(3\right)$$
333	332	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(t\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)$$
334	332	oveq2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(3\right)Y\left(3\right)Z\left(t\right)=X\left(3\right)Y\left(3\right)Z\left(3\right)$$
335	333 334	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(t\right)+X\left(3\right)Y\left(3\right)Z\left(t\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)$$
336	331 335	oveq12d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(t\right)+X\left(3\right)Z\left(3\right)Y\left(t\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(t\right)+X\left(3\right)Y\left(3\right)Z\left(t\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)\right)$$
337	77 79 93	adddiri	$$⊢\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Z\left(2\right)Y\left(3\right)$$
338	65 82 93	mulassi	$$⊢X\left(3\right)Z\left(3\right)Y\left(3\right)=X\left(3\right)Z\left(3\right)Y\left(3\right)$$
339	337 338	oveq12i	$$⊢\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Z\left(2\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)$$
340	88 90 82	adddiri	$$⊢\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)=X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)$$
341	65 93 82	mulassi	$$⊢X\left(3\right)Y\left(3\right)Z\left(3\right)=X\left(3\right)Y\left(3\right)Z\left(3\right)$$
342	340 341	oveq12i	$$⊢\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)=X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)$$
343	339 342	oveq12i	$$⊢\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)\right)=\left(X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Z\left(2\right)Y\left(3\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)\right)$$
344	75 76 93	mulassi	$$⊢X\left(1\right)Z\left(1\right)Y\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(3\right)$$
345	56 78 93	mulassi	$$⊢X\left(2\right)Z\left(2\right)Y\left(3\right)=X\left(2\right)Z\left(2\right)Y\left(3\right)$$
346	78 93	mulcomi	$$⊢Z\left(2\right)Y\left(3\right)=Y\left(3\right)Z\left(2\right)$$
347	346	oveq2i	$$⊢X\left(2\right)Z\left(2\right)Y\left(3\right)=X\left(2\right)Y\left(3\right)Z\left(2\right)$$
348	345 347	eqtri	$$⊢X\left(2\right)Z\left(2\right)Y\left(3\right)=X\left(2\right)Y\left(3\right)Z\left(2\right)$$
349	344 348	oveq12i	$$⊢X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Z\left(2\right)Y\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)$$
350	349	oveq1i	$$⊢X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Z\left(2\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)=X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)$$
351	75 85 82	mulassi	$$⊢X\left(1\right)Y\left(1\right)Z\left(3\right)=X\left(1\right)Y\left(1\right)Z\left(3\right)$$
352	56 89 82	mulassi	$$⊢X\left(2\right)Y\left(2\right)Z\left(3\right)=X\left(2\right)Y\left(2\right)Z\left(3\right)$$
353	351 352	oveq12i	$$⊢X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)=X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)$$
354	93 82	mulcomi	$$⊢Y\left(3\right)Z\left(3\right)=Z\left(3\right)Y\left(3\right)$$
355	354	oveq2i	$$⊢X\left(3\right)Y\left(3\right)Z\left(3\right)=X\left(3\right)Z\left(3\right)Y\left(3\right)$$
356	353 355	oveq12i	$$⊢X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)=X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)$$
357	350 356	oveq12i	$$⊢\left(X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Z\left(2\right)Y\left(3\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)\right)=\left(X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)\right)$$
358	76 93	mulcomi	$$⊢Z\left(1\right)Y\left(3\right)=Y\left(3\right)Z\left(1\right)$$
359	358	oveq2i	$$⊢X\left(1\right)Z\left(1\right)Y\left(3\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)$$
360	359	oveq1i	$$⊢X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)$$
361	360	oveq1i	$$⊢X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)$$
362	361	oveq1i	$$⊢\left(X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)\right)=\left(X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)\right)$$
363	75 160	mulcli	$$⊢X\left(1\right)Y\left(3\right)Z\left(1\right)\in ℂ$$
364	56 195	mulcli	$$⊢X\left(2\right)Y\left(3\right)Z\left(2\right)\in ℂ$$
365	363 364	addcli	$$⊢X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\in ℂ$$
366	75 163	mulcli	$$⊢X\left(1\right)Y\left(1\right)Z\left(3\right)\in ℂ$$
367	56 193	mulcli	$$⊢X\left(2\right)Y\left(2\right)Z\left(3\right)\in ℂ$$
368	366 367	addcli	$$⊢X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\in ℂ$$
369	82 93	mulcli	$$⊢Z\left(3\right)Y\left(3\right)\in ℂ$$
370	65 369	mulcli	$$⊢X\left(3\right)Z\left(3\right)Y\left(3\right)\in ℂ$$
371		pnpcan2	$$⊢\left(X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\in ℂ\wedge X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\in ℂ\wedge X\left(3\right)Z\left(3\right)Y\left(3\right)\in ℂ\right)\to \left(X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\right)$$
372	365 368 370 371	mp3an	$$⊢\left(X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\right)$$
373		subadd4	$$⊢\left(\left(X\left(1\right)Y\left(3\right)Z\left(1\right)\in ℂ\wedge X\left(1\right)Y\left(1\right)Z\left(3\right)\in ℂ\right)\wedge \left(X\left(2\right)Y\left(2\right)Z\left(3\right)\in ℂ\wedge X\left(2\right)Y\left(3\right)Z\left(2\right)\in ℂ\right)\right)\to X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\right)$$
374	363 366 367 364 373	mp4an	$$⊢X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\right)$$
375	374	eqcomi	$$⊢X\left(1\right)Y\left(3\right)Z\left(1\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)$$
376	362 372 375	3eqtri	$$⊢\left(X\left(1\right)Z\left(1\right)Y\left(3\right)+X\left(2\right)Y\left(3\right)Z\left(2\right)\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(X\left(1\right)Y\left(1\right)Z\left(3\right)+X\left(2\right)Y\left(2\right)Z\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)$$
377	343 357 376	3eqtri	$$⊢\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(3\right)+X\left(3\right)Z\left(3\right)Y\left(3\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(3\right)+X\left(3\right)Y\left(3\right)Z\left(3\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)$$
378	336 377	eqtrdi	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)\right)Y\left(t\right)+X\left(3\right)Z\left(3\right)Y\left(t\right)-\left(\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)\right)Z\left(t\right)+X\left(3\right)Y\left(3\right)Z\left(t\right)\right)=X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)$$
379	326 378	eqtr2d	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(1\right)Y\left(3\right)Z\left(1\right)-X\left(1\right)Y\left(1\right)Z\left(3\right)-\left(X\left(2\right)Y\left(2\right)Z\left(3\right)-X\left(2\right)Y\left(3\right)Z\left(2\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
380	312 379	eqtrid	$$⊢\left(\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\wedge t=1+2\right)\to X\left(1\right)\left(Y\left(3\right)Z\left(1\right)-Y\left(1\right)Z\left(3\right)\right)-X\left(2\right)\left(Y\left(2\right)Z\left(3\right)-Y\left(3\right)Z\left(2\right)\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
381	305 309 380	3eqtrd	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` 3 ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) with typecode |-
382	300 303 381	3eqtrd	Could not format ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) : No typesetting found for |- ( ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) /\ t = ( 1 + 2 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) with typecode |-
383		simpr	$$⊢\left(X\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)$$
384	301	eqcomi	$$⊢3=1+2$$
385	384	oveq2i	$$⊢\left(1\dots 3\right)=\left(1\dots 1+2\right)$$
386		1z	$$⊢1\in \mathbb{Z}$$
387		fztp	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
388	386 387	ax-mp	$$⊢\left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
389	385 388	eqtri	$$⊢\left(1\dots 3\right)=\left\{1,1+1,1+2\right\}$$
390	383 389	eleqtrdi	$$⊢\left(X\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\}$$
391		eltpi	$$⊢t\in \left\{1,1+1,1+2\right\}\to \left(t=1\vee t=1+1\vee t=1+2\right)$$
392	390 391	syl	$$⊢\left(X\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)$$
393	179 298 382 392	mpjao3dan	Could not format ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) : No typesetting found for |- ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` t ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` t ) ) ) ) with typecode |-
394		fveq2	$$⊢k=t\to Y\left(k\right)=Y\left(t\right)$$
395	394	oveq2d	$$⊢k=t\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)$$
396		fveq2	$$⊢k=t\to Z\left(k\right)=Z\left(t\right)$$
397	396	oveq2d	$$⊢k=t\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)=\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
398	395 397	oveq12d	$$⊢k=t\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
399	23	a1i	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\in ℝ$$
400	26	a1i	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to Y:\left(1\dots 3\right)⟶ℝ$$
401	400 383	ffvelcdmd	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to Y\left(t\right)\in ℝ$$
402	399 401	remulcld	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)\in ℝ$$
403	36	a1i	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\in ℝ$$
404	39	a1i	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to Z:\left(1\dots 3\right)⟶ℝ$$
405	404 383	ffvelcdmd	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to Z\left(t\right)\in ℝ$$
406	403 405	remulcld	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to \left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)\in ℝ$$
407	402 406	resubcld	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to \left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)\in ℝ$$
408	11 398 383 407	fvmptd3	$$⊢\left(X\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge t\in \left(1\dots 3\right)\right)\to \left(k\in \left(1\dots 3\right)⟼\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(k\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(k\right)\right)\left(t\right)=\left(X\left(1\right)Z\left(1\right)+X\left(2\right)Z\left(2\right)+X\left(3\right)Z\left(3\right)\right)Y\left(t\right)-\left(X\left(1\right)Y\left(1\right)+X\left(2\right)Y\left(2\right)+X\left(3\right)Y\left(3\right)\right)Z\left(t\right)$$
409	393 408	eqtr4d	Could not format ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) ` t ) ) : No typesetting found for |- ( ( X e. ( RR ^m ( 1 ... 3 ) ) /\ t e. ( 1 ... 3 ) ) -> ( ( X crossp ( Y crossp Z ) ) ` t ) = ( ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) ` t ) ) with typecode |-
410	10 44 409	eqfnfvd	Could not format ( X e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) ) : No typesetting found for |- ( X e. ( RR ^m ( 1 ... 3 ) ) -> ( X crossp ( Y crossp Z ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) ) with typecode |-
411	1 410	ax-mp	Could not format ( X crossp ( Y crossp Z ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) : No typesetting found for |- ( X crossp ( Y crossp Z ) ) = ( k e. ( 1 ... 3 ) |-> ( ( ( ( ( ( X ` 1 ) x. ( Z ` 1 ) ) + ( ( X ` 2 ) x. ( Z ` 2 ) ) ) + ( ( X ` 3 ) x. ( Z ` 3 ) ) ) x. ( Y ` k ) ) - ( ( ( ( ( X ` 1 ) x. ( Y ` 1 ) ) + ( ( X ` 2 ) x. ( Y ` 2 ) ) ) + ( ( X ` 3 ) x. ( Y ` 3 ) ) ) x. ( Z ` k ) ) ) ) with typecode |-