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 ) ) |