Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
crossp3d.2 ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
crossp3d.3 ⊢ ( 𝜑 → 𝑍 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion crossp3d ( 𝜑 → ( 𝑋 ⊠ ( 𝑌 ⊠ 𝑍 ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑍 ‘ 1 ) ) + ( ( 𝑋 ‘ 2 ) · ( 𝑍 ‘ 2 ) ) ) + ( ( 𝑋 ‘ 3 ) · ( 𝑍 ‘ 3 ) ) ) · ( 𝑌 ‘ 𝑘 ) ) − ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 1 ) ) + ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 2 ) ) ) + ( ( 𝑋 ‘ 3 ) · ( 𝑌 ‘ 3 ) ) ) · ( 𝑍 ‘ 𝑘 ) ) ) ) )

Proof

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