Step |
Hyp |
Ref |
Expression |
1 |
|
lbsss.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lbsss.j |
⊢ 𝐽 = ( LBasis ‘ 𝑊 ) |
3 |
|
elfvdm |
⊢ ( 𝐵 ∈ ( LBasis ‘ 𝑊 ) → 𝑊 ∈ dom LBasis ) |
4 |
3 2
|
eleq2s |
⊢ ( 𝐵 ∈ 𝐽 → 𝑊 ∈ dom LBasis ) |
5 |
|
eqid |
⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) |
6 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) |
8 |
|
eqid |
⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 ) |
9 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) |
10 |
1 5 6 7 2 8 9
|
islbs |
⊢ ( 𝑊 ∈ dom LBasis → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ) |
11 |
4 10
|
syl |
⊢ ( 𝐵 ∈ 𝐽 → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ) |
12 |
11
|
ibi |
⊢ ( 𝐵 ∈ 𝐽 → ( 𝐵 ⊆ 𝑉 ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) |
13 |
12
|
simp1d |
⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉 ) |