Step |
Hyp |
Ref |
Expression |
1 |
|
lvecdim.1 |
⊢ 𝐽 = ( LBasis ‘ 𝑊 ) |
2 |
|
eqid |
⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) |
3 |
|
eqid |
⊢ ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) = ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
5 |
2 3 4
|
lssacsex |
⊢ ( 𝑊 ∈ LVec → ( ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) ) |
7 |
6
|
simpld |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ) |
8 |
|
eqid |
⊢ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) = ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) |
9 |
6
|
simprd |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) |
10 |
|
simp2 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ∈ 𝐽 ) |
11 |
2 3 4 8 1
|
lbsacsbs |
⊢ ( 𝑊 ∈ LVec → ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) ) ) |
12 |
11
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) ) ) |
13 |
10 12
|
mpbid |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) ) |
14 |
13
|
simpld |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ) |
15 |
|
simp3 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ 𝐽 ) |
16 |
2 3 4 8 1
|
lbsacsbs |
⊢ ( 𝑊 ∈ LVec → ( 𝑇 ∈ 𝐽 ↔ ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) ) ) |
17 |
16
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑇 ∈ 𝐽 ↔ ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) ) ) |
18 |
15 17
|
mpbid |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) ) |
19 |
18
|
simpld |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ) |
20 |
13
|
simprd |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) |
21 |
18
|
simprd |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) |
22 |
20 21
|
eqtr4d |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) ) |
23 |
7 3 8 9 14 19 22
|
acsexdimd |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ≈ 𝑇 ) |