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 ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )

Proof

Step Hyp Ref Expression
1 df-bj-rvec ℝ-Vec = ( LMod ∩ ( Scalar “ { ℝfld } ) )
2 1 elin2 ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝑉 ∈ ( Scalar “ { ℝ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 ( 𝑉 ∈ LMod → 𝑉 ∈ V )
8 eleq2 ( dom Scalar = V → ( 𝑉 ∈ dom Scalar ↔ 𝑉 ∈ V ) )
9 7 8 syl5ibrcom ( 𝑉 ∈ LMod → ( dom Scalar = V → 𝑉 ∈ dom Scalar ) )
10 9 anim2d ( 𝑉 ∈ LMod → ( ( Fun Scalar ∧ dom Scalar = V ) → ( Fun Scalar ∧ 𝑉 ∈ dom Scalar ) ) )
11 6 10 mpi ( 𝑉 ∈ LMod → ( Fun Scalar ∧ 𝑉 ∈ dom Scalar ) )
12 fvimacnv ( ( Fun Scalar ∧ 𝑉 ∈ dom Scalar ) → ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ 𝑉 ∈ ( Scalar “ { ℝfld } ) ) )
13 11 12 syl ( 𝑉 ∈ LMod → ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ 𝑉 ∈ ( Scalar “ { ℝfld } ) ) )
14 fvex ( Scalar ‘ 𝑉 ) ∈ V
15 14 elsn ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ ( Scalar ‘ 𝑉 ) = ℝfld )
16 13 15 bitr3di ( 𝑉 ∈ LMod → ( 𝑉 ∈ ( Scalar “ { ℝfld } ) ↔ ( Scalar ‘ 𝑉 ) = ℝfld ) )
17 16 pm5.32i ( ( 𝑉 ∈ LMod ∧ 𝑉 ∈ ( Scalar “ { ℝfld } ) ) ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )
18 2 17 bitri ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )