Theorem crossp3i

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

	Ref	Expression
Hypotheses	crossp3i.1	⊢ 𝑋 ∈ ( ℝ ↑m ( 1 ... 3 ) )
	crossp3i.2	⊢ 𝑌 ∈ ( ℝ ↑m ( 1 ... 3 ) )
	crossp3i.3	⊢ 𝑍 ∈ ( ℝ ↑m ( 1 ... 3 ) )
Assertion	crossp3i	⊢ ( 𝑋 ⊠ ( 𝑌 ⊠ 𝑍 ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑍 ‘ 1 ) ) + ( ( 𝑋 ‘ 2 ) · ( 𝑍 ‘ 2 ) ) ) + ( ( 𝑋 ‘ 3 ) · ( 𝑍 ‘ 3 ) ) ) · ( 𝑌 ‘ 𝑘 ) ) − ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 1 ) ) + ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 2 ) ) ) + ( ( 𝑋 ‘ 3 ) · ( 𝑌 ‘ 3 ) ) ) · ( 𝑍 ‘ 𝑘 ) ) ) )

Proof

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