Metamath Proof Explorer

Theorem crosspclem

Description: Lemma for crosspcld . Closure of the three-way coordinate case split used in the cross product's mapping rule. (Contributed by Jiamin Zhao, 11-Aug-2026)

Ref Expression
Hypotheses crosspd.1 ⊢ φ → A ∈ ℝ 1 … 3
crosspd.2 ⊢ φ → B ∈ ℝ 1 … 3
Assertion crosspclem ⊢ φ → if k = 1 A ⁡ 2 ⁢ B ⁡ 3 − A ⁡ 3 ⁢ B ⁡ 2 if k = 2 A ⁡ 3 ⁢ B ⁡ 1 − A ⁡ 1 ⁢ B ⁡ 3 A ⁡ 1 ⁢ B ⁡ 2 − A ⁡ 2 ⁢ B ⁡ 1 ∈ ℝ

Proof

Step Hyp Ref Expression
1 crosspd.1 ⊢ φ → A ∈ ℝ 1 … 3
2 crosspd.2 ⊢ φ → B ∈ ℝ 1 … 3
3 1 2 crosspcle1d ⊢ φ → A ⁡ 2 ⁢ B ⁡ 3 − A ⁡ 3 ⁢ B ⁡ 2 ∈ ℝ
4 1 2 crosspcle2d ⊢ φ → A ⁡ 3 ⁢ B ⁡ 1 − A ⁡ 1 ⁢ B ⁡ 3 ∈ ℝ
5 1 2 crosspcle3d ⊢ φ → A ⁡ 1 ⁢ B ⁡ 2 − A ⁡ 2 ⁢ B ⁡ 1 ∈ ℝ
6 4 5 ifcld ⊢ φ → if k = 2 A ⁡ 3 ⁢ B ⁡ 1 − A ⁡ 1 ⁢ B ⁡ 3 A ⁡ 1 ⁢ B ⁡ 2 − A ⁡ 2 ⁢ B ⁡ 1 ∈ ℝ
7 3 6 ifcld ⊢ φ → if k = 1 A ⁡ 2 ⁢ B ⁡ 3 − A ⁡ 3 ⁢ B ⁡ 2 if k = 2 A ⁡ 3 ⁢ B ⁡ 1 − A ⁡ 1 ⁢ B ⁡ 3 A ⁡ 1 ⁢ B ⁡ 2 − A ⁡ 2 ⁢ B ⁡ 1 ∈ ℝ