Description: Closure of the second component of the cross product's Sarrus expansion. (A helper for crosspclifi and crosspv2i .) (Contributed by Jiamin Zhao, 31-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | crosspcle.1 | ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) | |
| crosspcle.2 | ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) | ||
| Assertion | crosspcle2i | ⊢ ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) ∈ ℝ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | crosspcle.1 | ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) | |
| 2 | crosspcle.2 | ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) | |
| 3 | 1 | rr3fv3cli | ⊢ ( 𝐴 ‘ 3 ) ∈ ℝ |
| 4 | 2 | rr3fv1cli | ⊢ ( 𝐵 ‘ 1 ) ∈ ℝ |
| 5 | 3 4 | remulcli | ⊢ ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) ∈ ℝ |
| 6 | 1 | rr3fv1cli | ⊢ ( 𝐴 ‘ 1 ) ∈ ℝ |
| 7 | 2 | rr3fv3cli | ⊢ ( 𝐵 ‘ 3 ) ∈ ℝ |
| 8 | 6 7 | remulcli | ⊢ ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ∈ ℝ |
| 9 | 5 8 | resubcli | ⊢ ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) ∈ ℝ |