| Step |
Hyp |
Ref |
Expression |
| 1 |
|
drngring |
⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring ) |
| 2 |
|
eqid |
⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 ) |
| 3 |
2
|
frlmlmod |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod ) |
| 4 |
1 3
|
sylan |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod ) |
| 5 |
|
eqid |
⊢ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) |
| 6 |
|
eqid |
⊢ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) |
| 7 |
5 6
|
lssmre |
⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod → ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 8 |
4 7
|
syl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 9 |
8
|
3adant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 10 |
|
eqid |
⊢ ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) = ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 11 |
|
eqid |
⊢ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) = ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 12 |
2
|
frlmsca |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 13 |
|
simpl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ DivRing ) |
| 14 |
12 13
|
eqeltrrd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ DivRing ) |
| 15 |
|
eqid |
⊢ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) |
| 16 |
15
|
islvec |
⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ↔ ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ DivRing ) ) |
| 17 |
4 14 16
|
sylanbrc |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec ) |
| 18 |
6 10 5
|
lssacsex |
⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec → ( ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ ( ACS ‘ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) ) |
| 19 |
17 18
|
syl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ ( ACS ‘ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) ) |
| 20 |
19
|
simprd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ∀ 𝑥 ∈ 𝒫 ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) |
| 21 |
20
|
3adant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ∀ 𝑥 ∈ 𝒫 ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) |
| 22 |
|
dif0 |
⊢ ( ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∖ ∅ ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) |
| 23 |
22
|
linds1 |
⊢ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑋 ⊆ ( ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∖ ∅ ) ) |
| 24 |
23
|
3ad2ant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∖ ∅ ) ) |
| 25 |
|
eqid |
⊢ ( 𝑅 unitVec 𝐼 ) = ( 𝑅 unitVec 𝐼 ) |
| 26 |
25 2 5
|
uvcff |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ) → ( 𝑅 unitVec 𝐼 ) : 𝐼 ⟶ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 27 |
1 26
|
sylan |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 unitVec 𝐼 ) : 𝐼 ⟶ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 28 |
27
|
frnd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ran ( 𝑅 unitVec 𝐼 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 29 |
28 22
|
sseqtrrdi |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ran ( 𝑅 unitVec 𝐼 ) ⊆ ( ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∖ ∅ ) ) |
| 30 |
29
|
3adant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ran ( 𝑅 unitVec 𝐼 ) ⊆ ( ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∖ ∅ ) ) |
| 31 |
5
|
linds1 |
⊢ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 32 |
31
|
3ad2ant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 33 |
|
un0 |
⊢ ( ran ( 𝑅 unitVec 𝐼 ) ∪ ∅ ) = ran ( 𝑅 unitVec 𝐼 ) |
| 34 |
33
|
fveq2i |
⊢ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( ran ( 𝑅 unitVec 𝐼 ) ∪ ∅ ) ) = ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) |
| 35 |
|
eqid |
⊢ ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) |
| 36 |
6 35 10
|
mrclsp |
⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod → ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 37 |
4 36
|
syl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 38 |
37
|
fveq1d |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) = ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) ) |
| 39 |
|
eqid |
⊢ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) |
| 40 |
2 25 39
|
frlmlbs |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 41 |
1 40
|
sylan |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 42 |
5 39 35
|
lbssp |
⊢ ( ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 43 |
41 42
|
syl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 44 |
38 43
|
eqtr3d |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 45 |
34 44
|
eqtrid |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( ran ( 𝑅 unitVec 𝐼 ) ∪ ∅ ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 46 |
45
|
3adant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( ran ( 𝑅 unitVec 𝐼 ) ∪ ∅ ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
| 47 |
32 46
|
sseqtrrd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( ran ( 𝑅 unitVec 𝐼 ) ∪ ∅ ) ) ) |
| 48 |
|
un0 |
⊢ ( 𝑋 ∪ ∅ ) = 𝑋 |
| 49 |
|
drngnzr |
⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing ) |
| 50 |
49
|
adantr |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ NzRing ) |
| 51 |
12 50
|
eqeltrrd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) |
| 52 |
4 51
|
jca |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ) |
| 53 |
35 15
|
lindsind2 |
⊢ ( ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 54 |
53
|
3expa |
⊢ ( ( ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 55 |
52 54
|
sylanl1 |
⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 56 |
37
|
fveq1d |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) = ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 57 |
56
|
eleq2d |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ↔ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) ) |
| 58 |
57
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ↔ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) ) |
| 59 |
55 58
|
mtbid |
⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 60 |
59
|
ralrimiva |
⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 61 |
60
|
3impa |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) |
| 62 |
10 11
|
ismri2 |
⊢ ( ( ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) ) |
| 63 |
8 31 62
|
syl2an |
⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) ) |
| 64 |
63
|
3impa |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) ) |
| 65 |
61 64
|
mpbird |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 66 |
48 65
|
eqeltrid |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) |
| 67 |
|
simpr |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝐼 ∈ Fin ) |
| 68 |
25
|
uvcendim |
⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ Fin ) → 𝐼 ≈ ran ( 𝑅 unitVec 𝐼 ) ) |
| 69 |
49 68
|
sylan |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝐼 ≈ ran ( 𝑅 unitVec 𝐼 ) ) |
| 70 |
|
enfi |
⊢ ( 𝐼 ≈ ran ( 𝑅 unitVec 𝐼 ) → ( 𝐼 ∈ Fin ↔ ran ( 𝑅 unitVec 𝐼 ) ∈ Fin ) ) |
| 71 |
69 70
|
syl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝐼 ∈ Fin ↔ ran ( 𝑅 unitVec 𝐼 ) ∈ Fin ) ) |
| 72 |
67 71
|
mpbid |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ran ( 𝑅 unitVec 𝐼 ) ∈ Fin ) |
| 73 |
72
|
olcd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ Fin ∨ ran ( 𝑅 unitVec 𝐼 ) ∈ Fin ) ) |
| 74 |
73
|
3adant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∈ Fin ∨ ran ( 𝑅 unitVec 𝐼 ) ∈ Fin ) ) |
| 75 |
9 10 11 21 24 30 47 66 74
|
mreexexd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ∃ 𝑓 ∈ 𝒫 ran ( 𝑅 unitVec 𝐼 ) ( 𝑋 ≈ 𝑓 ∧ ( 𝑓 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) ) |
| 76 |
|
simpl |
⊢ ( ( 𝑋 ≈ 𝑓 ∧ ( 𝑓 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) → 𝑋 ≈ 𝑓 ) |
| 77 |
|
ovex |
⊢ ( 𝑅 unitVec 𝐼 ) ∈ V |
| 78 |
77
|
rnex |
⊢ ran ( 𝑅 unitVec 𝐼 ) ∈ V |
| 79 |
|
elpwi |
⊢ ( 𝑓 ∈ 𝒫 ran ( 𝑅 unitVec 𝐼 ) → 𝑓 ⊆ ran ( 𝑅 unitVec 𝐼 ) ) |
| 80 |
|
ssdomg |
⊢ ( ran ( 𝑅 unitVec 𝐼 ) ∈ V → ( 𝑓 ⊆ ran ( 𝑅 unitVec 𝐼 ) → 𝑓 ≼ ran ( 𝑅 unitVec 𝐼 ) ) ) |
| 81 |
78 79 80
|
mpsyl |
⊢ ( 𝑓 ∈ 𝒫 ran ( 𝑅 unitVec 𝐼 ) → 𝑓 ≼ ran ( 𝑅 unitVec 𝐼 ) ) |
| 82 |
|
endomtr |
⊢ ( ( 𝑋 ≈ 𝑓 ∧ 𝑓 ≼ ran ( 𝑅 unitVec 𝐼 ) ) → 𝑋 ≼ ran ( 𝑅 unitVec 𝐼 ) ) |
| 83 |
76 81 82
|
syl2anr |
⊢ ( ( 𝑓 ∈ 𝒫 ran ( 𝑅 unitVec 𝐼 ) ∧ ( 𝑋 ≈ 𝑓 ∧ ( 𝑓 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) ) → 𝑋 ≼ ran ( 𝑅 unitVec 𝐼 ) ) |
| 84 |
83
|
rexlimiva |
⊢ ( ∃ 𝑓 ∈ 𝒫 ran ( 𝑅 unitVec 𝐼 ) ( 𝑋 ≈ 𝑓 ∧ ( 𝑓 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) → 𝑋 ≼ ran ( 𝑅 unitVec 𝐼 ) ) |
| 85 |
75 84
|
syl |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ≼ ran ( 𝑅 unitVec 𝐼 ) ) |
| 86 |
69
|
ensymd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ran ( 𝑅 unitVec 𝐼 ) ≈ 𝐼 ) |
| 87 |
86
|
3adant3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ran ( 𝑅 unitVec 𝐼 ) ≈ 𝐼 ) |
| 88 |
|
domentr |
⊢ ( ( 𝑋 ≼ ran ( 𝑅 unitVec 𝐼 ) ∧ ran ( 𝑅 unitVec 𝐼 ) ≈ 𝐼 ) → 𝑋 ≼ 𝐼 ) |
| 89 |
85 87 88
|
syl2anc |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ≼ 𝐼 ) |