Step | Hyp | Ref
| Expression |
1 | | drngring 19774 |
. . . . . . 7
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
2 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) |
3 | 2 | frlmlmod 20711 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod) |
4 | 1, 3 | sylan 583 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod) |
5 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅
freeLMod 𝐼)) =
(Base‘(𝑅 freeLMod
𝐼)) |
6 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘(𝑅
freeLMod 𝐼)) =
(LSubSp‘(𝑅 freeLMod
𝐼)) |
7 | 5, 6 | lssmre 20003 |
. . . . . 6
⊢ ((𝑅 freeLMod 𝐼) ∈ LMod → (LSubSp‘(𝑅 freeLMod 𝐼)) ∈ (Moore‘(Base‘(𝑅 freeLMod 𝐼)))) |
8 | 4, 7 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(LSubSp‘(𝑅 freeLMod
𝐼)) ∈
(Moore‘(Base‘(𝑅
freeLMod 𝐼)))) |
9 | 8 | 3adant3 1134 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (LSubSp‘(𝑅 freeLMod 𝐼)) ∈ (Moore‘(Base‘(𝑅 freeLMod 𝐼)))) |
10 | | eqid 2737 |
. . . 4
⊢
(mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼))) = (mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼))) |
11 | | eqid 2737 |
. . . 4
⊢
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) = (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) |
12 | 2 | frlmsca 20715 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼))) |
13 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈
DivRing) |
14 | 12, 13 | eqeltrrd 2839 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(Scalar‘(𝑅 freeLMod
𝐼)) ∈
DivRing) |
15 | | eqid 2737 |
. . . . . . . . 9
⊢
(Scalar‘(𝑅
freeLMod 𝐼)) =
(Scalar‘(𝑅 freeLMod
𝐼)) |
16 | 15 | islvec 20141 |
. . . . . . . 8
⊢ ((𝑅 freeLMod 𝐼) ∈ LVec ↔ ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ DivRing)) |
17 | 4, 14, 16 | sylanbrc 586 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LVec) |
18 | 6, 10, 5 | lssacsex 20181 |
. . . . . . 7
⊢ ((𝑅 freeLMod 𝐼) ∈ LVec → ((LSubSp‘(𝑅 freeLMod 𝐼)) ∈ (ACS‘(Base‘(𝑅 freeLMod 𝐼))) ∧ ∀𝑥 ∈ 𝒫 (Base‘(𝑅 freeLMod 𝐼))∀𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))∀𝑧 ∈ (((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑦})) ∖
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘𝑥))𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑧})))) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSubSp‘(𝑅 freeLMod
𝐼)) ∈
(ACS‘(Base‘(𝑅
freeLMod 𝐼))) ∧
∀𝑥 ∈ 𝒫
(Base‘(𝑅 freeLMod
𝐼))∀𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))∀𝑧 ∈ (((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑦})) ∖
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘𝑥))𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑧})))) |
20 | 19 | simprd 499 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
∀𝑥 ∈ 𝒫
(Base‘(𝑅 freeLMod
𝐼))∀𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))∀𝑧 ∈ (((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑦})) ∖
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘𝑥))𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑧}))) |
21 | 20 | 3adant3 1134 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∀𝑥 ∈ 𝒫 (Base‘(𝑅 freeLMod 𝐼))∀𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))∀𝑧 ∈ (((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑦})) ∖
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘𝑥))𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑧}))) |
22 | | dif0 4287 |
. . . . . 6
⊢
((Base‘(𝑅
freeLMod 𝐼)) ∖
∅) = (Base‘(𝑅
freeLMod 𝐼)) |
23 | 22 | linds1 20772 |
. . . . 5
⊢ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) → 𝑋 ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
24 | 23 | 3ad2ant3 1137 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
25 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼) |
26 | 25, 2, 5 | uvcff 20753 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼))) |
27 | 1, 26 | sylan 583 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼))) |
28 | 27 | frnd 6553 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
29 | 28, 22 | sseqtrrdi 3952 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
30 | 29 | 3adant3 1134 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ran (𝑅 unitVec 𝐼) ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
31 | 5 | linds1 20772 |
. . . . . 6
⊢ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) → 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
32 | 31 | 3ad2ant3 1137 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
33 | | un0 4305 |
. . . . . . . 8
⊢ (ran
(𝑅 unitVec 𝐼) ∪ ∅) = ran (𝑅 unitVec 𝐼) |
34 | 33 | fveq2i 6720 |
. . . . . . 7
⊢
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅)) =
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘ran (𝑅 unitVec 𝐼)) |
35 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(LSpan‘(𝑅
freeLMod 𝐼)) =
(LSpan‘(𝑅 freeLMod
𝐼)) |
36 | 6, 35, 10 | mrclsp 20026 |
. . . . . . . . . 10
⊢ ((𝑅 freeLMod 𝐼) ∈ LMod → (LSpan‘(𝑅 freeLMod 𝐼)) = (mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
37 | 4, 36 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(LSpan‘(𝑅 freeLMod
𝐼)) =
(mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
38 | 37 | fveq1d 6719 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSpan‘(𝑅 freeLMod
𝐼))‘ran (𝑅 unitVec 𝐼)) = ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘ran (𝑅 unitVec 𝐼))) |
39 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(LBasis‘(𝑅
freeLMod 𝐼)) =
(LBasis‘(𝑅 freeLMod
𝐼)) |
40 | 2, 25, 39 | frlmlbs 20759 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ∈ (LBasis‘(𝑅 freeLMod 𝐼))) |
41 | 1, 40 | sylan 583 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ∈ (LBasis‘(𝑅 freeLMod 𝐼))) |
42 | 5, 39, 35 | lbssp 20116 |
. . . . . . . . 9
⊢ (ran
(𝑅 unitVec 𝐼) ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran (𝑅 unitVec 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSpan‘(𝑅 freeLMod
𝐼))‘ran (𝑅 unitVec 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))) |
44 | 38, 43 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘ran (𝑅 unitVec 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))) |
45 | 34, 44 | syl5eq 2790 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅)) = (Base‘(𝑅 freeLMod 𝐼))) |
46 | 45 | 3adant3 1134 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) →
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅)) = (Base‘(𝑅 freeLMod 𝐼))) |
47 | 32, 46 | sseqtrrd 3942 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅))) |
48 | | un0 4305 |
. . . . 5
⊢ (𝑋 ∪ ∅) = 𝑋 |
49 | | drngnzr 20300 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
50 | 49 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing) |
51 | 12, 50 | eqeltrrd 2839 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(Scalar‘(𝑅 freeLMod
𝐼)) ∈
NzRing) |
52 | 4, 51 | jca 515 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)) |
53 | 35, 15 | lindsind2 20781 |
. . . . . . . . . . 11
⊢ ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) |
54 | 53 | 3expa 1120 |
. . . . . . . . . 10
⊢
(((((𝑅 freeLMod
𝐼) ∈ LMod ∧
(Scalar‘(𝑅 freeLMod
𝐼)) ∈ NzRing) ∧
𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) |
55 | 52, 54 | sylanl1 680 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) |
56 | 37 | fveq1d 6719 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSpan‘(𝑅 freeLMod
𝐼))‘(𝑋 ∖ {𝑦})) = ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
57 | 56 | eleq2d 2823 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) ↔ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
58 | 57 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) ↔ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
59 | 55, 58 | mtbid 327 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
60 | 59 | ralrimiva 3105 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
61 | 60 | 3impa 1112 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
62 | 10, 11 | ismri2 17135 |
. . . . . . . 8
⊢
(((LSubSp‘(𝑅
freeLMod 𝐼)) ∈
(Moore‘(Base‘(𝑅
freeLMod 𝐼))) ∧ 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) ↔ ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
63 | 8, 31, 62 | syl2an 599 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) ↔ ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
64 | 63 | 3impa 1112 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) ↔ ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
65 | 61, 64 | mpbird 260 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
66 | 48, 65 | eqeltrid 2842 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
67 | | simpr 488 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝐼 ∈ Fin) |
68 | 25 | uvcendim 20809 |
. . . . . . . . 9
⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ Fin) → 𝐼 ≈ ran (𝑅 unitVec 𝐼)) |
69 | 49, 68 | sylan 583 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝐼 ≈ ran (𝑅 unitVec 𝐼)) |
70 | | enfi 8865 |
. . . . . . . 8
⊢ (𝐼 ≈ ran (𝑅 unitVec 𝐼) → (𝐼 ∈ Fin ↔ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
71 | 69, 70 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝐼 ∈ Fin ↔ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
72 | 67, 71 | mpbid 235 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ∈ Fin) |
73 | 72 | olcd 874 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑋 ∈ Fin ∨ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
74 | 73 | 3adant3 1134 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ Fin ∨ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
75 | 9, 10, 11, 21, 24, 30, 47, 66, 74 | mreexexd 17151 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∃𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼)(𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))))) |
76 | | simpl 486 |
. . . . 5
⊢ ((𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) → 𝑋 ≈ 𝑓) |
77 | | ovex 7246 |
. . . . . . 7
⊢ (𝑅 unitVec 𝐼) ∈ V |
78 | 77 | rnex 7690 |
. . . . . 6
⊢ ran
(𝑅 unitVec 𝐼) ∈ V |
79 | | elpwi 4522 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼) → 𝑓 ⊆ ran (𝑅 unitVec 𝐼)) |
80 | | ssdomg 8674 |
. . . . . 6
⊢ (ran
(𝑅 unitVec 𝐼) ∈ V → (𝑓 ⊆ ran (𝑅 unitVec 𝐼) → 𝑓 ≼ ran (𝑅 unitVec 𝐼))) |
81 | 78, 79, 80 | mpsyl 68 |
. . . . 5
⊢ (𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼) → 𝑓 ≼ ran (𝑅 unitVec 𝐼)) |
82 | | endomtr 8686 |
. . . . 5
⊢ ((𝑋 ≈ 𝑓 ∧ 𝑓 ≼ ran (𝑅 unitVec 𝐼)) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
83 | 76, 81, 82 | syl2anr 600 |
. . . 4
⊢ ((𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼) ∧ (𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))))) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
84 | 83 | rexlimiva 3200 |
. . 3
⊢
(∃𝑓 ∈
𝒫 ran (𝑅 unitVec
𝐼)(𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
85 | 75, 84 | syl 17 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
86 | 69 | ensymd 8679 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ≈ 𝐼) |
87 | 86 | 3adant3 1134 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ran (𝑅 unitVec 𝐼) ≈ 𝐼) |
88 | | domentr 8687 |
. 2
⊢ ((𝑋 ≼ ran (𝑅 unitVec 𝐼) ∧ ran (𝑅 unitVec 𝐼) ≈ 𝐼) → 𝑋 ≼ 𝐼) |
89 | 85, 87, 88 | syl2anc 587 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼) |