Description: The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-isrvecd.scal | ⊢ ( 𝜑 → ( Scalar ‘ 𝑉 ) = 𝐾 ) | |
Assertion | bj-isrvecd | ⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-isrvecd.scal | ⊢ ( 𝜑 → ( Scalar ‘ 𝑉 ) = 𝐾 ) | |
2 | bj-isrvec | ⊢ ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) ) | |
3 | 1 | eqeq1d | ⊢ ( 𝜑 → ( ( Scalar ‘ 𝑉 ) = ℝfld ↔ 𝐾 = ℝfld ) ) |
4 | 3 | anbi2d | ⊢ ( 𝜑 → ( ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) ) |
5 | 2 4 | syl5bb | ⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) ) |