Theorem crosspalti 50667

Description: Antisymmetry of the cross product: swapping the two vectors negates the result. (Contributed by Jiamin Zhao, 1-Aug-2026.)

Hypotheses

Ref	Expression
crosspalti.1	⊢ 𝐴 ∈ (ℝ ↑m (1...3))
crosspalti.2	⊢ 𝐵 ∈ (ℝ ↑m (1...3))

Assertion

Ref	Expression
crosspalti	⊢ (𝐴⊠𝐵) = (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘))

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘

Proof of Theorem crosspalti

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		crosspalti.1	. 2 ⊢ 𝐴 ∈ (ℝ ↑m (1...3))
2		crosspalti.2	. . . . . 6 ⊢ 𝐵 ∈ (ℝ ↑m (1...3))
3	1, 2	crosspcli 50660	. . . . 5 ⊢ (𝐴⊠𝐵) ∈ (ℝ ↑m (1...3))
4		elmapfn 8858	. . . . 5 ⊢ ((𝐴⊠𝐵) ∈ (ℝ ↑m (1...3)) → (𝐴⊠𝐵) Fn (1...3))
5	3, 4	ax-mp 5	. . . 4 ⊢ (𝐴⊠𝐵) Fn (1...3)
6	5	a1i 11	. . 3 ⊢ (𝐴 ∈ (ℝ ↑m (1...3)) → (𝐴⊠𝐵) Fn (1...3))
7		negex 11450	. . . . 5 ⊢ -((𝐵⊠𝐴)‘𝑘) ∈ V
8		eqid 2763	. . . . 5 ⊢ (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘)) = (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘))
9	7, 8	fnmpti 6678	. . . 4 ⊢ (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘)) Fn (1...3)
10	9	a1i 11	. . 3 ⊢ (𝐴 ∈ (ℝ ↑m (1...3)) → (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘)) Fn (1...3))
11		simpr 489	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → 𝑡 = 1)
12	11	fveq2d 6885	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐴⊠𝐵)‘𝑡) = ((𝐴⊠𝐵)‘1))
13	1, 2	crosspv1i 50661	. . . . . . 7 ⊢ ((𝐴⊠𝐵)‘1) = (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2)))
14	12, 13	eqtrdi 2814	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐴⊠𝐵)‘𝑡) = (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))))
15	1	rr3fv2cli 50649	. . . . . . . . . . . 12 ⊢ (𝐴‘2) ∈ ℝ
16	15	recni 11218	. . . . . . . . . . 11 ⊢ (𝐴‘2) ∈ ℂ
17	2	rr3fv3cli 50650	. . . . . . . . . . . 12 ⊢ (𝐵‘3) ∈ ℝ
18	17	recni 11218	. . . . . . . . . . 11 ⊢ (𝐵‘3) ∈ ℂ
19	16, 18	mulcomi 11212	. . . . . . . . . 10 ⊢ ((𝐴‘2) · (𝐵‘3)) = ((𝐵‘3) · (𝐴‘2))
20	19	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐴‘2) · (𝐵‘3)) = ((𝐵‘3) · (𝐴‘2)))
21	1	rr3fv3cli 50650	. . . . . . . . . . . 12 ⊢ (𝐴‘3) ∈ ℝ
22	21	recni 11218	. . . . . . . . . . 11 ⊢ (𝐴‘3) ∈ ℂ
23	2	rr3fv2cli 50649	. . . . . . . . . . . 12 ⊢ (𝐵‘2) ∈ ℝ
24	23	recni 11218	. . . . . . . . . . 11 ⊢ (𝐵‘2) ∈ ℂ
25	22, 24	mulcomi 11212	. . . . . . . . . 10 ⊢ ((𝐴‘3) · (𝐵‘2)) = ((𝐵‘2) · (𝐴‘3))
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐴‘3) · (𝐵‘2)) = ((𝐵‘2) · (𝐴‘3)))
27	20, 26	oveq12d 7428	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))) = (((𝐵‘3) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘3))))
28	23, 21	remulcli 11220	. . . . . . . . . 10 ⊢ ((𝐵‘2) · (𝐴‘3)) ∈ ℝ
29	28	recni 11218	. . . . . . . . 9 ⊢ ((𝐵‘2) · (𝐴‘3)) ∈ ℂ
30	17, 15	remulcli 11220	. . . . . . . . . 10 ⊢ ((𝐵‘3) · (𝐴‘2)) ∈ ℝ
31	30	recni 11218	. . . . . . . . 9 ⊢ ((𝐵‘3) · (𝐴‘2)) ∈ ℂ
32	29, 31	negsubdi2i 11539	. . . . . . . 8 ⊢ -(((𝐵‘2) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘2))) = (((𝐵‘3) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘3)))
33	27, 32	eqtr4di 2816	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))) = -(((𝐵‘2) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘2))))
34	11	fveq2d 6885	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐵⊠𝐴)‘𝑡) = ((𝐵⊠𝐴)‘1))
35	2, 1	crosspv1i 50661	. . . . . . . . 9 ⊢ ((𝐵⊠𝐴)‘1) = (((𝐵‘2) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘2)))
36	34, 35	eqtrdi 2814	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐵⊠𝐴)‘𝑡) = (((𝐵‘2) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘2))))
37	36	negeqd 11446	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → -((𝐵⊠𝐴)‘𝑡) = -(((𝐵‘2) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘2))))
38	33, 37	eqtr4d 2801	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))) = -((𝐵⊠𝐴)‘𝑡))
39	14, 38	eqtrd 2798	. . . . 5 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = 1) → ((𝐴⊠𝐵)‘𝑡) = -((𝐵⊠𝐴)‘𝑡))
40	2, 1	crosspv2i 50662	. . . . . . . . . 10 ⊢ ((𝐵⊠𝐴)‘2) = (((𝐵‘3) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘3)))
41	40	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → ((𝐵⊠𝐴)‘2) = (((𝐵‘3) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘3))))
42	41	negeqd 11446	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → -((𝐵⊠𝐴)‘2) = -(((𝐵‘3) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘3))))
43	1	rr3fv1cli 50648	. . . . . . . . . . . 12 ⊢ (𝐴‘1) ∈ ℝ
44	17, 43	remulcli 11220	. . . . . . . . . . 11 ⊢ ((𝐵‘3) · (𝐴‘1)) ∈ ℝ
45	44	recni 11218	. . . . . . . . . 10 ⊢ ((𝐵‘3) · (𝐴‘1)) ∈ ℂ
46	2	rr3fv1cli 50648	. . . . . . . . . . 11 ⊢ (𝐵‘1) ∈ ℝ
47		remulcl 11180	. . . . . . . . . . . 12 ⊢ (((𝐵‘1) ∈ ℝ ∧ (𝐴‘3) ∈ ℝ) → ((𝐵‘1) · (𝐴‘3)) ∈ ℝ)
48	47	recnd 11232	. . . . . . . . . . 11 ⊢ (((𝐵‘1) ∈ ℝ ∧ (𝐴‘3) ∈ ℝ) → ((𝐵‘1) · (𝐴‘3)) ∈ ℂ)
49	46, 21, 48	mp2an 704	. . . . . . . . . 10 ⊢ ((𝐵‘1) · (𝐴‘3)) ∈ ℂ
50	45, 49	negsubdi2i 11539	. . . . . . . . 9 ⊢ -(((𝐵‘3) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘3))) = (((𝐵‘1) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘1)))
51	46	recni 11218	. . . . . . . . . . . 12 ⊢ (𝐵‘1) ∈ ℂ
52	51, 22	mulcomi 11212	. . . . . . . . . . 11 ⊢ ((𝐵‘1) · (𝐴‘3)) = ((𝐴‘3) · (𝐵‘1))
53	52	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → ((𝐵‘1) · (𝐴‘3)) = ((𝐴‘3) · (𝐵‘1)))
54	43	recni 11218	. . . . . . . . . . . 12 ⊢ (𝐴‘1) ∈ ℂ
55	18, 54	mulcomi 11212	. . . . . . . . . . 11 ⊢ ((𝐵‘3) · (𝐴‘1)) = ((𝐴‘1) · (𝐵‘3))
56	55	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → ((𝐵‘3) · (𝐴‘1)) = ((𝐴‘1) · (𝐵‘3)))
57	53, 56	oveq12d 7428	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → (((𝐵‘1) · (𝐴‘3)) − ((𝐵‘3) · (𝐴‘1))) = (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))))
58	50, 57	eqtrid 2810	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → -(((𝐵‘3) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘3))) = (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))))
59	42, 58	eqtrd 2798	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → -((𝐵⊠𝐴)‘2) = (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))))
60	1, 2	crosspv2i 50662	. . . . . . 7 ⊢ ((𝐴⊠𝐵)‘2) = (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3)))
61	59, 60	eqtr4di 2816	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → -((𝐵⊠𝐴)‘2) = ((𝐴⊠𝐵)‘2))
62		simpr 489	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → 𝑡 = (1 + 1))
63		1p1e2 12359	. . . . . . . . 9 ⊢ (1 + 1) = 2
64	62, 63	eqtrdi 2814	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → 𝑡 = 2)
65	64	fveq2d 6885	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → ((𝐵⊠𝐴)‘𝑡) = ((𝐵⊠𝐴)‘2))
66	65	negeqd 11446	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → -((𝐵⊠𝐴)‘𝑡) = -((𝐵⊠𝐴)‘2))
67	64	fveq2d 6885	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → ((𝐴⊠𝐵)‘𝑡) = ((𝐴⊠𝐵)‘2))
68	61, 66, 67	3eqtr4rd 2809	. . . . 5 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 1)) → ((𝐴⊠𝐵)‘𝑡) = -((𝐵⊠𝐴)‘𝑡))
69	2, 1	crosspv3i 50663	. . . . . . . . . 10 ⊢ ((𝐵⊠𝐴)‘3) = (((𝐵‘1) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘1)))
70	69	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → ((𝐵⊠𝐴)‘3) = (((𝐵‘1) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘1))))
71	70	negeqd 11446	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → -((𝐵⊠𝐴)‘3) = -(((𝐵‘1) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘1))))
72	46, 15	remulcli 11220	. . . . . . . . . . 11 ⊢ ((𝐵‘1) · (𝐴‘2)) ∈ ℝ
73	72	recni 11218	. . . . . . . . . 10 ⊢ ((𝐵‘1) · (𝐴‘2)) ∈ ℂ
74		remulcl 11180	. . . . . . . . . . . 12 ⊢ (((𝐵‘2) ∈ ℝ ∧ (𝐴‘1) ∈ ℝ) → ((𝐵‘2) · (𝐴‘1)) ∈ ℝ)
75	74	recnd 11232	. . . . . . . . . . 11 ⊢ (((𝐵‘2) ∈ ℝ ∧ (𝐴‘1) ∈ ℝ) → ((𝐵‘2) · (𝐴‘1)) ∈ ℂ)
76	23, 43, 75	mp2an 704	. . . . . . . . . 10 ⊢ ((𝐵‘2) · (𝐴‘1)) ∈ ℂ
77	73, 76	negsubdi2i 11539	. . . . . . . . 9 ⊢ -(((𝐵‘1) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘1))) = (((𝐵‘2) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘2)))
78	24, 54	mulcomi 11212	. . . . . . . . . . 11 ⊢ ((𝐵‘2) · (𝐴‘1)) = ((𝐴‘1) · (𝐵‘2))
79	78	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → ((𝐵‘2) · (𝐴‘1)) = ((𝐴‘1) · (𝐵‘2)))
80	51, 16	mulcomi 11212	. . . . . . . . . . 11 ⊢ ((𝐵‘1) · (𝐴‘2)) = ((𝐴‘2) · (𝐵‘1))
81	80	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → ((𝐵‘1) · (𝐴‘2)) = ((𝐴‘2) · (𝐵‘1)))
82	79, 81	oveq12d 7428	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → (((𝐵‘2) · (𝐴‘1)) − ((𝐵‘1) · (𝐴‘2))) = (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1))))
83	77, 82	eqtrid 2810	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → -(((𝐵‘1) · (𝐴‘2)) − ((𝐵‘2) · (𝐴‘1))) = (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1))))
84	71, 83	eqtrd 2798	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → -((𝐵⊠𝐴)‘3) = (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1))))
85	1, 2	crosspv3i 50663	. . . . . . 7 ⊢ ((𝐴⊠𝐵)‘3) = (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1)))
86	84, 85	eqtr4di 2816	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → -((𝐵⊠𝐴)‘3) = ((𝐴⊠𝐵)‘3))
87		simpr 489	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → 𝑡 = (1 + 2))
88		1p2e3 12378	. . . . . . . . 9 ⊢ (1 + 2) = 3
89	87, 88	eqtrdi 2814	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → 𝑡 = 3)
90	89	fveq2d 6885	. . . . . . 7 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → ((𝐵⊠𝐴)‘𝑡) = ((𝐵⊠𝐴)‘3))
91	90	negeqd 11446	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → -((𝐵⊠𝐴)‘𝑡) = -((𝐵⊠𝐴)‘3))
92	89	fveq2d 6885	. . . . . 6 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → ((𝐴⊠𝐵)‘𝑡) = ((𝐴⊠𝐵)‘3))
93	86, 91, 92	3eqtr4rd 2809	. . . . 5 ⊢ (((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) ∧ 𝑡 = (1 + 2)) → ((𝐴⊠𝐵)‘𝑡) = -((𝐵⊠𝐴)‘𝑡))
94		simpr 489	. . . . . . 7 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → 𝑡 ∈ (1...3))
95	88	eqcomi 2772	. . . . . . . . 9 ⊢ 3 = (1 + 2)
96	95	oveq2i 7421	. . . . . . . 8 ⊢ (1...3) = (1...(1 + 2))
97		1z 12619	. . . . . . . . 9 ⊢ 1 ∈ ℤ
98		fztp 13604	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (1...(1 + 2)) = {1, (1 + 1), (1 + 2)})
99	97, 98	ax-mp 5	. . . . . . . 8 ⊢ (1...(1 + 2)) = {1, (1 + 1), (1 + 2)}
100	96, 99	eqtri 2786	. . . . . . 7 ⊢ (1...3) = {1, (1 + 1), (1 + 2)}
101	94, 100	eleqtrdi 2873	. . . . . 6 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → 𝑡 ∈ {1, (1 + 1), (1 + 2)})
102		eltpi 4654	. . . . . 6 ⊢ (𝑡 ∈ {1, (1 + 1), (1 + 2)} → (𝑡 = 1 ∨ 𝑡 = (1 + 1) ∨ 𝑡 = (1 + 2)))
103	101, 102	syl 18	. . . . 5 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → (𝑡 = 1 ∨ 𝑡 = (1 + 1) ∨ 𝑡 = (1 + 2)))
104	39, 68, 93, 103	mpjao3dan 1459	. . . 4 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → ((𝐴⊠𝐵)‘𝑡) = -((𝐵⊠𝐴)‘𝑡))
105		fveq2 6881	. . . . . 6 ⊢ (𝑘 = 𝑡 → ((𝐵⊠𝐴)‘𝑘) = ((𝐵⊠𝐴)‘𝑡))
106	105	negeqd 11446	. . . . 5 ⊢ (𝑘 = 𝑡 → -((𝐵⊠𝐴)‘𝑘) = -((𝐵⊠𝐴)‘𝑡))
107		negex 11450	. . . . . 6 ⊢ -((𝐵⊠𝐴)‘𝑡) ∈ V
108	107	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → -((𝐵⊠𝐴)‘𝑡) ∈ V)
109	8, 106, 94, 108	fvmptd3 7013	. . . 4 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → ((𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘))‘𝑡) = -((𝐵⊠𝐴)‘𝑡))
110	104, 109	eqtr4d 2801	. . 3 ⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝑡 ∈ (1...3)) → ((𝐴⊠𝐵)‘𝑡) = ((𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘))‘𝑡))
111	6, 10, 110	eqfnfvd 7028	. 2 ⊢ (𝐴 ∈ (ℝ ↑m (1...3)) → (𝐴⊠𝐵) = (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘)))
112	1, 111	ax-mp 5	1 ⊢ (𝐴⊠𝐵) = (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘))

Syntax hints:   ∧ wa 400   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {ctp 4593   ↦ cmpt 5192   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410   ↑_m cmap 8820  ℂcc 11093  ℝcr 11094  1c1 11096   + caddc 11098   · cmul 11100   − cmin 11436  -cneg 11437  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)