Metamath Proof Explorer

Theorem bj-isrvec

Description: The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-isrvec ⊢ V ∈ ℝVec ↔ V ∈ LMod ∧ Scalar ⁡ V = ℝ fld

Proof

Step Hyp Ref Expression
1 df-bj-rvec ⊢ ℝVec = LMod ∩ Scalar -1 ℝ fld
2 1 elin2 ⊢ V ∈ ℝVec ↔ V ∈ LMod ∧ V ∈ Scalar -1 ℝ fld
3 bj-evalfun ⊢ Fun ⁡ Slot 5
4 df-sca ⊢ Scalar = Slot 5
5 4 funeqi ⊢ Fun ⁡ Scalar ↔ Fun ⁡ Slot 5
6 3 5 mpbir ⊢ Fun ⁡ Scalar
7 0re ⊢ 0 ∈ ℝ
8 7 n0ii ⊢ ¬ ℝ = ∅
9 eqcom ⊢ ∅ = ℝ ↔ ℝ = ∅
10 8 9 mtbir ⊢ ¬ ∅ = ℝ
11 fveq2 ⊢ ∅ = ℝ fld → Base ∅ = Base ℝ fld
12 base0 ⊢ ∅ = Base ∅
13 rebase ⊢ ℝ = Base ℝ fld
14 11 12 13 3eqtr4g ⊢ ∅ = ℝ fld → ∅ = ℝ
15 10 14 mto ⊢ ¬ ∅ = ℝ fld
16 elsni ⊢ ∅ ∈ ℝ fld → ∅ = ℝ fld
17 15 16 mto ⊢ ¬ ∅ ∈ ℝ fld
18 bj-fvimacnv0 ⊢ Fun ⁡ Scalar ∧ ¬ ∅ ∈ ℝ fld → Scalar ⁡ V ∈ ℝ fld ↔ V ∈ Scalar -1 ℝ fld
19 6 17 18 mp2an ⊢ Scalar ⁡ V ∈ ℝ fld ↔ V ∈ Scalar -1 ℝ fld
20 fvex ⊢ Scalar ⁡ V ∈ V
21 20 elsn ⊢ Scalar ⁡ V ∈ ℝ fld ↔ Scalar ⁡ V = ℝ fld
22 19 21 bitr3i ⊢ V ∈ Scalar -1 ℝ fld ↔ Scalar ⁡ V = ℝ fld
23 22 anbi2i ⊢ V ∈ LMod ∧ V ∈ Scalar -1 ℝ fld ↔ V ∈ LMod ∧ Scalar ⁡ V = ℝ fld
24 2 23 bitri ⊢ V ∈ ℝVec ↔ V ∈ LMod ∧ Scalar ⁡ V = ℝ fld