Proof of Theorem lvecendof1f1o
| Step | Hyp | Ref
| Expression |
| 1 | | lvecendof1f1o.1 |
. 2
⊢ (𝜑 → 𝑈:𝐵–1-1→𝐵) |
| 2 | | lvecendof1f1o.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (𝐸 LMHom 𝐸)) |
| 3 | | lvecendof1f1o.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐸) |
| 4 | 3, 3 | lmhmf 21033 |
. . . . 5
⊢ (𝑈 ∈ (𝐸 LMHom 𝐸) → 𝑈:𝐵⟶𝐵) |
| 5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈:𝐵⟶𝐵) |
| 6 | 5 | ffnd 6737 |
. . 3
⊢ (𝜑 → 𝑈 Fn 𝐵) |
| 7 | | lvecendof1f1o.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ LVec) |
| 8 | | lvecendof1f1o.d |
. . . 4
⊢ (𝜑 → (dim‘𝐸) ∈
ℕ0) |
| 9 | | lmhmrnlss 21049 |
. . . . 5
⊢ (𝑈 ∈ (𝐸 LMHom 𝐸) → ran 𝑈 ∈ (LSubSp‘𝐸)) |
| 10 | 2, 9 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑈 ∈ (LSubSp‘𝐸)) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐸) = (0g‘𝐸) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢ (𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})) = (𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢ (𝐸 ↾s ran 𝑈) = (𝐸 ↾s ran 𝑈) |
| 14 | 11, 12, 13 | dimkerim 33678 |
. . . . . 6
⊢ ((𝐸 ∈ LVec ∧ 𝑈 ∈ (𝐸 LMHom 𝐸)) → (dim‘𝐸) = ((dim‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) +𝑒
(dim‘(𝐸
↾s ran 𝑈)))) |
| 15 | 7, 2, 14 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (dim‘𝐸) = ((dim‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) +𝑒
(dim‘(𝐸
↾s ran 𝑈)))) |
| 16 | | eqid 2737 |
. . . . . . . . . 10
⊢ (◡𝑈 “ {(0g‘𝐸)}) = (◡𝑈 “ {(0g‘𝐸)}) |
| 17 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LSubSp‘𝐸) =
(LSubSp‘𝐸) |
| 18 | 16, 11, 17 | lmhmkerlss 21050 |
. . . . . . . . 9
⊢ (𝑈 ∈ (𝐸 LMHom 𝐸) → (◡𝑈 “ {(0g‘𝐸)}) ∈ (LSubSp‘𝐸)) |
| 19 | 2, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑈 “ {(0g‘𝐸)}) ∈ (LSubSp‘𝐸)) |
| 20 | 12, 17 | lsslvec 21108 |
. . . . . . . 8
⊢ ((𝐸 ∈ LVec ∧ (◡𝑈 “ {(0g‘𝐸)}) ∈ (LSubSp‘𝐸)) → (𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})) ∈
LVec) |
| 21 | 7, 19, 20 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})) ∈
LVec) |
| 22 | 2 | lmhmghmd 33042 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (𝐸 GrpHom 𝐸)) |
| 23 | 3, 3, 11, 11 | kerf1ghm 19265 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (𝐸 GrpHom 𝐸) → (𝑈:𝐵–1-1→𝐵 ↔ (◡𝑈 “ {(0g‘𝐸)}) =
{(0g‘𝐸)})) |
| 24 | 23 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (𝐸 GrpHom 𝐸) ∧ 𝑈:𝐵–1-1→𝐵) → (◡𝑈 “ {(0g‘𝐸)}) =
{(0g‘𝐸)}) |
| 25 | 22, 1, 24 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑈 “ {(0g‘𝐸)}) =
{(0g‘𝐸)}) |
| 26 | | cnvimass 6100 |
. . . . . . . . . 10
⊢ (◡𝑈 “ {(0g‘𝐸)}) ⊆ dom 𝑈 |
| 27 | 26, 5 | fssdm 6755 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝑈 “ {(0g‘𝐸)}) ⊆ 𝐵) |
| 28 | 12, 3 | ressbas2 17283 |
. . . . . . . . 9
⊢ ((◡𝑈 “ {(0g‘𝐸)}) ⊆ 𝐵 → (◡𝑈 “ {(0g‘𝐸)}) = (Base‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})))) |
| 29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑈 “ {(0g‘𝐸)}) = (Base‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})))) |
| 30 | 7 | lvecgrpd 21107 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ Grp) |
| 31 | 30 | grpmndd 18964 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ Mnd) |
| 32 | 3, 11 | mndidcl 18762 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ Mnd →
(0g‘𝐸)
∈ 𝐵) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0g‘𝐸) ∈ 𝐵) |
| 34 | 11, 11 | ghmid 19240 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ (𝐸 GrpHom 𝐸) → (𝑈‘(0g‘𝐸)) = (0g‘𝐸)) |
| 35 | 22, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈‘(0g‘𝐸)) = (0g‘𝐸)) |
| 36 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(0g‘𝐸) ∈ V |
| 37 | 36 | snid 4662 |
. . . . . . . . . . . 12
⊢
(0g‘𝐸) ∈ {(0g‘𝐸)} |
| 38 | 35, 37 | eqeltrdi 2849 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈‘(0g‘𝐸)) ∈
{(0g‘𝐸)}) |
| 39 | 6, 33, 38 | elpreimad 7079 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝐸) ∈ (◡𝑈 “ {(0g‘𝐸)})) |
| 40 | 12, 3, 11 | ress0g 18775 |
. . . . . . . . . 10
⊢ ((𝐸 ∈ Mnd ∧
(0g‘𝐸)
∈ (◡𝑈 “ {(0g‘𝐸)}) ∧ (◡𝑈 “ {(0g‘𝐸)}) ⊆ 𝐵) → (0g‘𝐸) = (0g‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})))) |
| 41 | 31, 39, 27, 40 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝐸) = (0g‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})))) |
| 42 | 41 | sneqd 4638 |
. . . . . . . 8
⊢ (𝜑 →
{(0g‘𝐸)} =
{(0g‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)})))}) |
| 43 | 25, 29, 42 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (𝜑 → (Base‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) =
{(0g‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)})))}) |
| 44 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) =
(0g‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)}))) |
| 45 | 44 | lvecdim0 33657 |
. . . . . . . 8
⊢ ((𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})) ∈ LVec →
((dim‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)}))) = 0 ↔
(Base‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)}))) =
{(0g‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)})))})) |
| 46 | 45 | biimpar 477 |
. . . . . . 7
⊢ (((𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)})) ∈ LVec ∧
(Base‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)}))) =
{(0g‘(𝐸
↾s (◡𝑈 “ {(0g‘𝐸)})))}) → (dim‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) = 0) |
| 47 | 21, 43, 46 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (dim‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) = 0) |
| 48 | 47 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((dim‘(𝐸 ↾s (◡𝑈 “ {(0g‘𝐸)}))) +𝑒
(dim‘(𝐸
↾s ran 𝑈))) = (0 +𝑒
(dim‘(𝐸
↾s ran 𝑈)))) |
| 49 | 13, 17 | lsslvec 21108 |
. . . . . . 7
⊢ ((𝐸 ∈ LVec ∧ ran 𝑈 ∈ (LSubSp‘𝐸)) → (𝐸 ↾s ran 𝑈) ∈ LVec) |
| 50 | 7, 10, 49 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐸 ↾s ran 𝑈) ∈ LVec) |
| 51 | | dimcl 33653 |
. . . . . 6
⊢ ((𝐸 ↾s ran 𝑈) ∈ LVec →
(dim‘(𝐸
↾s ran 𝑈))
∈ ℕ0*) |
| 52 | | xnn0xr 12604 |
. . . . . 6
⊢
((dim‘(𝐸
↾s ran 𝑈))
∈ ℕ0* → (dim‘(𝐸 ↾s ran 𝑈)) ∈
ℝ*) |
| 53 | | xaddlid 13284 |
. . . . . 6
⊢
((dim‘(𝐸
↾s ran 𝑈))
∈ ℝ* → (0 +𝑒 (dim‘(𝐸 ↾s ran 𝑈))) = (dim‘(𝐸 ↾s ran 𝑈))) |
| 54 | 50, 51, 52, 53 | 4syl 19 |
. . . . 5
⊢ (𝜑 → (0 +𝑒
(dim‘(𝐸
↾s ran 𝑈))) = (dim‘(𝐸 ↾s ran 𝑈))) |
| 55 | 15, 48, 54 | 3eqtrrd 2782 |
. . . 4
⊢ (𝜑 → (dim‘(𝐸 ↾s ran 𝑈)) = (dim‘𝐸)) |
| 56 | 3, 7, 8, 10, 55 | dimlssid 33683 |
. . 3
⊢ (𝜑 → ran 𝑈 = 𝐵) |
| 57 | | df-fo 6567 |
. . 3
⊢ (𝑈:𝐵–onto→𝐵 ↔ (𝑈 Fn 𝐵 ∧ ran 𝑈 = 𝐵)) |
| 58 | 6, 56, 57 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝑈:𝐵–onto→𝐵) |
| 59 | | df-f1o 6568 |
. 2
⊢ (𝑈:𝐵–1-1-onto→𝐵 ↔ (𝑈:𝐵–1-1→𝐵 ∧ 𝑈:𝐵–onto→𝐵)) |
| 60 | 1, 58, 59 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑈:𝐵–1-1-onto→𝐵) |