Step | Hyp | Ref
| Expression |
1 | | drngring 18577 |
. . . . . . 7
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
2 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) |
3 | 2 | frlmlmod 19912 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod) |
4 | 1, 3 | sylan 487 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑅
freeLMod 𝐼)) =
(Base‘(𝑅 freeLMod
𝐼)) |
6 | | eqid 2610 |
. . . . . . 7
⊢
(LSubSp‘(𝑅
freeLMod 𝐼)) =
(LSubSp‘(𝑅 freeLMod
𝐼)) |
7 | 5, 6 | lssmre 18787 |
. . . . . 6
⊢ ((𝑅 freeLMod 𝐼) ∈ LMod → (LSubSp‘(𝑅 freeLMod 𝐼)) ∈ (Moore‘(Base‘(𝑅 freeLMod 𝐼)))) |
8 | 4, 7 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(LSubSp‘(𝑅 freeLMod
𝐼)) ∈
(Moore‘(Base‘(𝑅
freeLMod 𝐼)))) |
9 | 8 | 3adant3 1074 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (LSubSp‘(𝑅 freeLMod 𝐼)) ∈ (Moore‘(Base‘(𝑅 freeLMod 𝐼)))) |
10 | | eqid 2610 |
. . . 4
⊢
(mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼))) = (mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼))) |
11 | | eqid 2610 |
. . . 4
⊢
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) = (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) |
12 | 2 | frlmsca 19916 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼))) |
13 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈
DivRing) |
14 | 12, 13 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(Scalar‘(𝑅 freeLMod
𝐼)) ∈
DivRing) |
15 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘(𝑅
freeLMod 𝐼)) =
(Scalar‘(𝑅 freeLMod
𝐼)) |
16 | 15 | islvec 18925 |
. . . . . . . 8
⊢ ((𝑅 freeLMod 𝐼) ∈ LVec ↔ ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ DivRing)) |
17 | 4, 14, 16 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LVec) |
18 | 6, 10, 5 | lssacsex 18965 |
. . . . . . 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 478 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
∀𝑥 ∈ 𝒫
(Base‘(𝑅 freeLMod
𝐼))∀𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))∀𝑧 ∈ (((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑦})) ∖
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘𝑥))𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑧}))) |
21 | 20 | 3adant3 1074 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∀𝑥 ∈ 𝒫 (Base‘(𝑅 freeLMod 𝐼))∀𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))∀𝑧 ∈ (((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑦})) ∖
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘𝑥))𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑥 ∪ {𝑧}))) |
22 | | dif0 3904 |
. . . . . 6
⊢
((Base‘(𝑅
freeLMod 𝐼)) ∖
∅) = (Base‘(𝑅
freeLMod 𝐼)) |
23 | 22 | linds1 19968 |
. . . . 5
⊢ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) → 𝑋 ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
24 | 23 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
25 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼) |
26 | 25, 2, 5 | uvcff 19949 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼))) |
27 | 1, 26 | sylan 487 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼))) |
28 | | frn 5966 |
. . . . . . 7
⊢ ((𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)) → ran (𝑅 unitVec 𝐼) ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
30 | 29, 22 | syl6sseqr 3615 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
31 | 30 | 3adant3 1074 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ran (𝑅 unitVec 𝐼) ⊆ ((Base‘(𝑅 freeLMod 𝐼)) ∖ ∅)) |
32 | 5 | linds1 19968 |
. . . . . 6
⊢ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) → 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
33 | 32 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) |
34 | | un0 3919 |
. . . . . . . 8
⊢ (ran
(𝑅 unitVec 𝐼) ∪ ∅) = ran (𝑅 unitVec 𝐼) |
35 | 34 | fveq2i 6106 |
. . . . . . 7
⊢
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅)) =
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘ran (𝑅 unitVec 𝐼)) |
36 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(LSpan‘(𝑅
freeLMod 𝐼)) =
(LSpan‘(𝑅 freeLMod
𝐼)) |
37 | 6, 36, 10 | mrclsp 18810 |
. . . . . . . . . 10
⊢ ((𝑅 freeLMod 𝐼) ∈ LMod → (LSpan‘(𝑅 freeLMod 𝐼)) = (mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
38 | 4, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(LSpan‘(𝑅 freeLMod
𝐼)) =
(mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
39 | 38 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSpan‘(𝑅 freeLMod
𝐼))‘ran (𝑅 unitVec 𝐼)) = ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘ran (𝑅 unitVec 𝐼))) |
40 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(LBasis‘(𝑅
freeLMod 𝐼)) =
(LBasis‘(𝑅 freeLMod
𝐼)) |
41 | 2, 25, 40 | frlmlbs 19955 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ∈ (LBasis‘(𝑅 freeLMod 𝐼))) |
42 | 1, 41 | sylan 487 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ∈ (LBasis‘(𝑅 freeLMod 𝐼))) |
43 | 5, 40, 36 | lbssp 18900 |
. . . . . . . . 9
⊢ (ran
(𝑅 unitVec 𝐼) ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran (𝑅 unitVec 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSpan‘(𝑅 freeLMod
𝐼))‘ran (𝑅 unitVec 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))) |
45 | 39, 44 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘ran (𝑅 unitVec 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))) |
46 | 35, 45 | syl5eq 2656 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅)) = (Base‘(𝑅 freeLMod 𝐼))) |
47 | 46 | 3adant3 1074 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) →
((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅)) = (Base‘(𝑅 freeLMod 𝐼))) |
48 | 33, 47 | sseqtr4d 3605 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(ran (𝑅 unitVec 𝐼) ∪ ∅))) |
49 | | un0 3919 |
. . . . 5
⊢ (𝑋 ∪ ∅) = 𝑋 |
50 | | drngnzr 19083 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing) |
52 | 12, 51 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(Scalar‘(𝑅 freeLMod
𝐼)) ∈
NzRing) |
53 | 4, 52 | jca 553 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)) |
54 | 36, 15 | lindsind2 19977 |
. . . . . . . . . . 11
⊢ ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) |
55 | 54 | 3expa 1257 |
. . . . . . . . . 10
⊢
(((((𝑅 freeLMod
𝐼) ∈ LMod ∧
(Scalar‘(𝑅 freeLMod
𝐼)) ∈ NzRing) ∧
𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) |
56 | 53, 55 | sylanl1 680 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) |
57 | 38 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
((LSpan‘(𝑅 freeLMod
𝐼))‘(𝑋 ∖ {𝑦})) = ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
58 | 57 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) ↔ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
59 | 58 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) ↔ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
60 | 56, 59 | mtbid 313 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ 𝑋) → ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
61 | 60 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
62 | 61 | 3impa 1251 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦}))) |
63 | 10, 11 | ismri2 16115 |
. . . . . . . 8
⊢
(((LSubSp‘(𝑅
freeLMod 𝐼)) ∈
(Moore‘(Base‘(𝑅
freeLMod 𝐼))) ∧ 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) ↔ ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
64 | 8, 32, 63 | syl2an 493 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) ↔ ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
65 | 64 | 3impa 1251 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))) ↔ ∀𝑦 ∈ 𝑋 ¬ 𝑦 ∈ ((mrCls‘(LSubSp‘(𝑅 freeLMod 𝐼)))‘(𝑋 ∖ {𝑦})))) |
66 | 62, 65 | mpbird 246 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ∈ (mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
67 | 49, 66 | syl5eqel 2692 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) |
68 | | simpr 476 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝐼 ∈ Fin) |
69 | 25 | uvcendim 20005 |
. . . . . . . . 9
⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ Fin) → 𝐼 ≈ ran (𝑅 unitVec 𝐼)) |
70 | 50, 69 | sylan 487 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝐼 ≈ ran (𝑅 unitVec 𝐼)) |
71 | | enfi 8061 |
. . . . . . . 8
⊢ (𝐼 ≈ ran (𝑅 unitVec 𝐼) → (𝐼 ∈ Fin ↔ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
72 | 70, 71 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝐼 ∈ Fin ↔ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
73 | 68, 72 | mpbid 221 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ∈ Fin) |
74 | 73 | olcd 407 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑋 ∈ Fin ∨ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
75 | 74 | 3adant3 1074 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∈ Fin ∨ ran (𝑅 unitVec 𝐼) ∈ Fin)) |
76 | 9, 10, 11, 21, 24, 31, 48, 67, 75 | mreexexd 16131 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ∃𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼)(𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))))) |
77 | | simpl 472 |
. . . . 5
⊢ ((𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) → 𝑋 ≈ 𝑓) |
78 | | ovex 6577 |
. . . . . . 7
⊢ (𝑅 unitVec 𝐼) ∈ V |
79 | 78 | rnex 6992 |
. . . . . 6
⊢ ran
(𝑅 unitVec 𝐼) ∈ V |
80 | | elpwi 4117 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼) → 𝑓 ⊆ ran (𝑅 unitVec 𝐼)) |
81 | | ssdomg 7887 |
. . . . . 6
⊢ (ran
(𝑅 unitVec 𝐼) ∈ V → (𝑓 ⊆ ran (𝑅 unitVec 𝐼) → 𝑓 ≼ ran (𝑅 unitVec 𝐼))) |
82 | 79, 80, 81 | mpsyl 66 |
. . . . 5
⊢ (𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼) → 𝑓 ≼ ran (𝑅 unitVec 𝐼)) |
83 | | endomtr 7900 |
. . . . 5
⊢ ((𝑋 ≈ 𝑓 ∧ 𝑓 ≼ ran (𝑅 unitVec 𝐼)) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
84 | 77, 82, 83 | syl2anr 494 |
. . . 4
⊢ ((𝑓 ∈ 𝒫 ran (𝑅 unitVec 𝐼) ∧ (𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼))))) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
85 | 84 | rexlimiva 3010 |
. . 3
⊢
(∃𝑓 ∈
𝒫 ran (𝑅 unitVec
𝐼)(𝑋 ≈ 𝑓 ∧ (𝑓 ∪ ∅) ∈
(mrInd‘(LSubSp‘(𝑅 freeLMod 𝐼)))) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
86 | 76, 85 | syl 17 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ ran (𝑅 unitVec 𝐼)) |
87 | 70 | ensymd 7893 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ran (𝑅 unitVec 𝐼) ≈ 𝐼) |
88 | 87 | 3adant3 1074 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ran (𝑅 unitVec 𝐼) ≈ 𝐼) |
89 | | domentr 7901 |
. 2
⊢ ((𝑋 ≼ ran (𝑅 unitVec 𝐼) ∧ ran (𝑅 unitVec 𝐼) ≈ 𝐼) → 𝑋 ≼ 𝐼) |
90 | 86, 88, 89 | syl2anc 691 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼) |