crossp3d - Mathbox for Jiamin Zhao

	Mathbox for Jiamin Zhao		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > crossp3d		Structured version Visualization version GIF version

Theorem crossp3d 50706

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

**Hypotheses**
Ref	Expression
crossp3d.1	⊢ (𝜑 → 𝑋 ∈ (ℝ ↑_m (1...3)))
crossp3d.2	⊢ (𝜑 → 𝑌 ∈ (ℝ ↑_m (1...3)))
crossp3d.3	⊢ (𝜑 → 𝑍 ∈ (ℝ ↑_m (1...3)))

**Assertion**
Ref	Expression
crossp3d	⊢ (𝜑 → (𝑋⊠(𝑌⊠𝑍)) = (𝑘 ∈ (1...3) ↦ ((((((𝑋‘1) · (𝑍‘1)) + ((𝑋‘2) · (𝑍‘2))) + ((𝑋‘3) · (𝑍‘3))) · (𝑌‘𝑘)) − (((((𝑋‘1) · (𝑌‘1)) + ((𝑋‘2) · (𝑌‘2))) + ((𝑋‘3) · (𝑌‘3))) · (𝑍‘𝑘)))))

Distinct variable groups: 𝑘,𝑋 𝑘,𝑌 𝑘,𝑍 Allowed substitution hint: 𝜑(𝑘)

Proof of Theorem crossp3d Dummy variable 𝑡 is distinct from all other variables.

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ w3o 1102 = wceq 1570 ∈ wcel 2146 {ctp 4595 ↦ cmpt 5194 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ↑_m cmap 8830 ℂcc 11113 ℝcr 11114 1c1 11116 + caddc 11118 · cmul 11120 − cmin 11456 2c2 12310 3c3 12311 ℤcz 12606 ...cfz 13551 ⊠ccrossp 50689

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-er 8700 df-map 8832 df-en 8950 df-dom 8951 df-sdom 8952 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-z 12607 df-uz 12879 df-fz 13552 df-crossp 50690

This theorem is used by: (None)

W3C validator