Theorem crossp3d

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, 12-Aug-2026)

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