Metamath Proof Explorer

Theorem bj-isrvec

Description: The predicate "is a real vector space". Using df-sca instead of scaid would shorten 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=SlotScalar⁡ndx
4 3 slotfn ⊢ScalarFnV
5 df-fn ⊢ScalarFnV↔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