crossp3i - Mathbox for Jiamin Zhao

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

Theorem crossp3i 50668

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 50652 rather than introducing a separate dot product operator. (Contributed by Jiamin Zhao, 1-Aug-2026.)

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

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

Distinct variable groups: 𝑘,𝑋 𝑘,𝑌 𝑘,𝑍

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

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

Colors of variables: wff setvar class

Syntax hints: ∧ wa 400 ∨ w3o 1102 = wceq 1570 ∈ wcel 2143 {ctp 4593 ↦ cmpt 5192 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ↑_m cmap 8820 ℂcc 11093 ℝcr 11094 1c1 11096 + caddc 11098 · cmul 11100 − cmin 11436 2c2 12290 3c3 12291 ℤcz 12586 ...cfz 13530 ⊠ccrossp 50651

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-z 12587 df-uz 12858 df-fz 13531 df-crossp 50652

This theorem is referenced by: (None)

W3C validator