Step |
Hyp |
Ref |
Expression |
1 |
|
bj-isrvec2.scal |
⊢ ( 𝜑 → ( Scalar ‘ 𝑉 ) = 𝐾 ) |
2 |
|
bj-rvecvec |
⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec ) |
3 |
2
|
a1i |
⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec ) ) |
4 |
|
bj-rvecrr |
⊢ ( 𝑉 ∈ ℝ-Vec → ( Scalar ‘ 𝑉 ) = ℝfld ) |
5 |
1
|
eqeq1d |
⊢ ( 𝜑 → ( ( Scalar ‘ 𝑉 ) = ℝfld ↔ 𝐾 = ℝfld ) ) |
6 |
4 5
|
syl5ib |
⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec → 𝐾 = ℝfld ) ) |
7 |
3 6
|
jcad |
⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec → ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) ) ) |
8 |
|
bj-vecssmodel |
⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod ) |
9 |
8
|
anim1i |
⊢ ( ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) → ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) |
10 |
1
|
bj-isrvecd |
⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) ) |
11 |
9 10
|
syl5ibr |
⊢ ( 𝜑 → ( ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) → 𝑉 ∈ ℝ-Vec ) ) |
12 |
7 11
|
impbid |
⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) ) ) |