Metamath Proof Explorer

Theorem bj-isrvec

Description: The predicate "is a real vector space". Using df-sca instead of scaid shortens the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca . (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 scaid ⊢ Scalar = Slot Scalar ⁡ ndx
4 3 slotfn ⊢ Scalar Fn V
5 df-fn ⊢ Scalar Fn V ↔ Fun ⁡ Scalar ∧ dom ⁡ Scalar = V
6 4 5 mpbi ⊢ Fun ⁡ Scalar ∧ dom ⁡ Scalar = V
7 elex ⊢ V ∈ LMod → V ∈ V
8 eleq2 ⊢ dom ⁡ Scalar = V → V ∈ dom ⁡ Scalar ↔ V ∈ V
9 7 8 syl5ibrcom ⊢ V ∈ LMod → dom ⁡ Scalar = V → V ∈ dom ⁡ Scalar
10 9 anim2d ⊢ V ∈ LMod → Fun ⁡ Scalar ∧ dom ⁡ Scalar = V → Fun ⁡ Scalar ∧ V ∈ dom ⁡ Scalar
11 6 10 mpi ⊢ V ∈ LMod → Fun ⁡ Scalar ∧ V ∈ dom ⁡ Scalar
12 fvimacnv ⊢ Fun ⁡ Scalar ∧ V ∈ dom ⁡ Scalar → Scalar ⁡ V ∈ ℝ fld ↔ V ∈ Scalar -1 ℝ fld
13 11 12 syl ⊢ V ∈ LMod → Scalar ⁡ V ∈ ℝ fld ↔ V ∈ Scalar -1 ℝ fld
14 fvex ⊢ Scalar ⁡ V ∈ V
15 14 elsn ⊢ Scalar ⁡ V ∈ ℝ fld ↔ Scalar ⁡ V = ℝ fld
16 13 15 bitr3di ⊢ V ∈ LMod → V ∈ Scalar -1 ℝ fld ↔ Scalar ⁡ V = ℝ fld
17 16 pm5.32i ⊢ V ∈ LMod ∧ V ∈ Scalar -1 ℝ fld ↔ V ∈ LMod ∧ Scalar ⁡ V = ℝ fld
18 2 17 bitri ⊢ V ∈ ℝVec ↔ V ∈ LMod ∧ Scalar ⁡ V = ℝ fld