| Step | Hyp | Ref
| Expression |
| 1 | | 0elpw 5356 |
. . 3
⊢ ∅
∈ 𝒫 (Base‘𝑀) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 3 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
| 4 | | eqid 2737 |
. . . 4
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
| 5 | 2, 3, 4 | lcoop 48328 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ ∅ ∈
𝒫 (Base‘𝑀))
→ (𝑀 LinCo ∅) =
{𝑣 ∈ (Base‘𝑀) ∣ ∃𝑤 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))}) |
| 6 | 1, 5 | mpan2 691 |
. 2
⊢ (𝑀 ∈ Mnd → (𝑀 LinCo ∅) = {𝑣 ∈ (Base‘𝑀) ∣ ∃𝑤 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))}) |
| 7 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
| 8 | | map0e 8922 |
. . . . . . 7
⊢
((Base‘(Scalar‘𝑀)) ∈ V →
((Base‘(Scalar‘𝑀)) ↑m ∅) =
1o) |
| 9 | 7, 8 | mp1i 13 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) →
((Base‘(Scalar‘𝑀)) ↑m ∅) =
1o) |
| 10 | | df1o2 8513 |
. . . . . 6
⊢
1o = {∅} |
| 11 | 9, 10 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) →
((Base‘(Scalar‘𝑀)) ↑m ∅) =
{∅}) |
| 12 | 11 | rexeqdv 3327 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ ∃𝑤 ∈ {∅} (𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)))) |
| 13 | | lincval0 48332 |
. . . . . . . 8
⊢ (𝑀 ∈ Mnd → (∅(
linC ‘𝑀)∅) =
(0g‘𝑀)) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∅( linC
‘𝑀)∅) =
(0g‘𝑀)) |
| 15 | 14 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑣 = (∅( linC ‘𝑀)∅) ↔ 𝑣 = (0g‘𝑀))) |
| 16 | 15 | anbi2d 630 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → ((∅ ∈ Fin
∧ 𝑣 = (∅( linC
‘𝑀)∅)) ↔
(∅ ∈ Fin ∧ 𝑣
= (0g‘𝑀)))) |
| 17 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 18 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤 finSupp
(0g‘(Scalar‘𝑀)) ↔ ∅ finSupp
(0g‘(Scalar‘𝑀)))) |
| 19 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(0g‘(Scalar‘𝑀)) ∈ V |
| 20 | | 0fsupp 9430 |
. . . . . . . . . . 11
⊢
((0g‘(Scalar‘𝑀)) ∈ V → ∅ finSupp
(0g‘(Scalar‘𝑀))) |
| 21 | 19, 20 | ax-mp 5 |
. . . . . . . . . 10
⊢ ∅
finSupp (0g‘(Scalar‘𝑀)) |
| 22 | | 0fi 9082 |
. . . . . . . . . 10
⊢ ∅
∈ Fin |
| 23 | 21, 22 | 2th 264 |
. . . . . . . . 9
⊢ (∅
finSupp (0g‘(Scalar‘𝑀)) ↔ ∅ ∈
Fin) |
| 24 | 18, 23 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑤 finSupp
(0g‘(Scalar‘𝑀)) ↔ ∅ ∈
Fin)) |
| 25 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤( linC ‘𝑀)∅) = (∅( linC ‘𝑀)∅)) |
| 26 | 25 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑣 = (𝑤( linC ‘𝑀)∅) ↔ 𝑣 = (∅( linC ‘𝑀)∅))) |
| 27 | 24, 26 | anbi12d 632 |
. . . . . . 7
⊢ (𝑤 = ∅ → ((𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧
𝑣 = (∅( linC
‘𝑀)∅)))) |
| 28 | 27 | rexsng 4676 |
. . . . . 6
⊢ (∅
∈ V → (∃𝑤
∈ {∅} (𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧
𝑣 = (∅( linC
‘𝑀)∅)))) |
| 29 | 17, 28 | mp1i 13 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈ {∅} (𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧
𝑣 = (∅( linC
‘𝑀)∅)))) |
| 30 | 22 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → ∅ ∈
Fin) |
| 31 | 30 | biantrurd 532 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑣 = (0g‘𝑀) ↔ (∅ ∈ Fin ∧ 𝑣 = (0g‘𝑀)))) |
| 32 | 16, 29, 31 | 3bitr4d 311 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈ {∅} (𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ 𝑣 = (0g‘𝑀))) |
| 33 | 12, 32 | bitrd 279 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ 𝑣 = (0g‘𝑀))) |
| 34 | 33 | rabbidva 3443 |
. 2
⊢ (𝑀 ∈ Mnd → {𝑣 ∈ (Base‘𝑀) ∣ ∃𝑤 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))} = {𝑣 ∈ (Base‘𝑀) ∣ 𝑣 = (0g‘𝑀)}) |
| 35 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 36 | 2, 35 | mndidcl 18762 |
. . 3
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
| 37 | | rabsn 4721 |
. . 3
⊢
((0g‘𝑀) ∈ (Base‘𝑀) → {𝑣 ∈ (Base‘𝑀) ∣ 𝑣 = (0g‘𝑀)} = {(0g‘𝑀)}) |
| 38 | 36, 37 | syl 17 |
. 2
⊢ (𝑀 ∈ Mnd → {𝑣 ∈ (Base‘𝑀) ∣ 𝑣 = (0g‘𝑀)} = {(0g‘𝑀)}) |
| 39 | 6, 34, 38 | 3eqtrd 2781 |
1
⊢ (𝑀 ∈ Mnd → (𝑀 LinCo ∅) =
{(0g‘𝑀)}) |