| Step | Hyp | Ref
| Expression |
| 1 | | lindsrng01.r |
. . . . . . . . 9
⊢ 𝑅 = (Scalar‘𝑀) |
| 2 | | lindsrng01.e |
. . . . . . . . 9
⊢ 𝐸 = (Base‘𝑅) |
| 3 | 1, 2 | lmodsn0 20872 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod → 𝐸 ≠ ∅) |
| 4 | 2 | fvexi 6920 |
. . . . . . . . . 10
⊢ 𝐸 ∈ V |
| 5 | | hasheq0 14402 |
. . . . . . . . . 10
⊢ (𝐸 ∈ V →
((♯‘𝐸) = 0
↔ 𝐸 =
∅)) |
| 6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
⊢
((♯‘𝐸) =
0 ↔ 𝐸 =
∅) |
| 7 | | eqneqall 2951 |
. . . . . . . . . 10
⊢ (𝐸 = ∅ → (𝐸 ≠ ∅ → 𝑆 linIndS 𝑀)) |
| 8 | 7 | com12 32 |
. . . . . . . . 9
⊢ (𝐸 ≠ ∅ → (𝐸 = ∅ → 𝑆 linIndS 𝑀)) |
| 9 | 6, 8 | biimtrid 242 |
. . . . . . . 8
⊢ (𝐸 ≠ ∅ →
((♯‘𝐸) = 0
→ 𝑆 linIndS 𝑀)) |
| 10 | 3, 9 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ LMod →
((♯‘𝐸) = 0
→ 𝑆 linIndS 𝑀)) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) → ((♯‘𝐸) = 0 → 𝑆 linIndS 𝑀)) |
| 12 | 11 | com12 32 |
. . . . 5
⊢
((♯‘𝐸) =
0 → ((𝑀 ∈ LMod
∧ 𝑆 ∈ 𝒫
𝐵) → 𝑆 linIndS 𝑀)) |
| 13 | 1 | lmodring 20866 |
. . . . . . . . 9
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Ring) |
| 14 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑅 ∈ Ring) |
| 15 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 16 | 2, 15 | 0ring 20526 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
(♯‘𝐸) = 1)
→ 𝐸 =
{(0g‘𝑅)}) |
| 17 | 14, 16 | sylan 580 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1) → 𝐸 = {(0g‘𝑅)}) |
| 18 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑆 ∈ 𝒫 𝐵) |
| 19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1) → 𝑆 ∈ 𝒫 𝐵) |
| 20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → 𝑆 ∈ 𝒫 𝐵) |
| 21 | | snex 5436 |
. . . . . . . . . . . . . 14
⊢
{(0g‘𝑅)} ∈ V |
| 22 | 19, 21 | jctil 519 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1) →
({(0g‘𝑅)}
∈ V ∧ 𝑆 ∈
𝒫 𝐵)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → ({(0g‘𝑅)} ∈ V ∧ 𝑆 ∈ 𝒫 𝐵)) |
| 24 | | elmapg 8879 |
. . . . . . . . . . . 12
⊢
(({(0g‘𝑅)} ∈ V ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑓 ∈ ({(0g‘𝑅)} ↑m 𝑆) ↔ 𝑓:𝑆⟶{(0g‘𝑅)})) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (𝑓 ∈ ({(0g‘𝑅)} ↑m 𝑆) ↔ 𝑓:𝑆⟶{(0g‘𝑅)})) |
| 26 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑅) ∈ V |
| 27 | 26 | fconst2 7225 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑆⟶{(0g‘𝑅)} ↔ 𝑓 = (𝑆 × {(0g‘𝑅)})) |
| 28 | | fconstmpt 5747 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ×
{(0g‘𝑅)})
= (𝑥 ∈ 𝑆 ↦
(0g‘𝑅)) |
| 29 | 28 | eqeq2i 2750 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑆 × {(0g‘𝑅)}) ↔ 𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅))) |
| 30 | 27, 29 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑓:𝑆⟶{(0g‘𝑅)} ↔ 𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅))) |
| 31 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) ∧ 𝑣 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅))) |
| 32 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) ∧ 𝑣 ∈ 𝑆) ∧ 𝑥 = 𝑣) → (0g‘𝑅) = (0g‘𝑅)) |
| 33 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ 𝑆) |
| 34 | | fvexd 6921 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) ∧ 𝑣 ∈ 𝑆) → (0g‘𝑅) ∈ V) |
| 35 | 31, 32, 33, 34 | fvmptd 7023 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) ∧ 𝑣 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣) = (0g‘𝑅)) |
| 36 | 35 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → ∀𝑣 ∈ 𝑆 ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣) = (0g‘𝑅)) |
| 37 | 36 | a1d 25 |
. . . . . . . . . . . . 13
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (((𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) finSupp
(0g‘𝑅)
∧ ((𝑥 ∈ 𝑆 ↦
(0g‘𝑅))(
linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣) = (0g‘𝑅))) |
| 38 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → (𝑓 finSupp (0g‘𝑅) ↔ (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) finSupp
(0g‘𝑅))) |
| 39 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → (𝑓( linC ‘𝑀)𝑆) = ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))( linC ‘𝑀)𝑆)) |
| 40 | 39 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → ((𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ↔ ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))( linC ‘𝑀)𝑆) = (0g‘𝑀))) |
| 41 | 38, 40 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → ((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) ↔ ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) finSupp
(0g‘𝑅)
∧ ((𝑥 ∈ 𝑆 ↦
(0g‘𝑅))(
linC ‘𝑀)𝑆) = (0g‘𝑀)))) |
| 42 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → (𝑓‘𝑣) = ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣)) |
| 43 | 42 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → ((𝑓‘𝑣) = (0g‘𝑅) ↔ ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣) = (0g‘𝑅))) |
| 44 | 43 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → (∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅) ↔ ∀𝑣 ∈ 𝑆 ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣) = (0g‘𝑅))) |
| 45 | 41, 44 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → (((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)) ↔ (((𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) finSupp
(0g‘𝑅)
∧ ((𝑥 ∈ 𝑆 ↦
(0g‘𝑅))(
linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 ((𝑥 ∈ 𝑆 ↦ (0g‘𝑅))‘𝑣) = (0g‘𝑅)))) |
| 46 | 37, 45 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (𝑓 = (𝑥 ∈ 𝑆 ↦ (0g‘𝑅)) → ((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)))) |
| 47 | 30, 46 | biimtrid 242 |
. . . . . . . . . . 11
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (𝑓:𝑆⟶{(0g‘𝑅)} → ((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)))) |
| 48 | 25, 47 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (𝑓 ∈ ({(0g‘𝑅)} ↑m 𝑆) → ((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)))) |
| 49 | 48 | ralrimiv 3145 |
. . . . . . . . 9
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → ∀𝑓 ∈ ({(0g‘𝑅)} ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅))) |
| 50 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝐸 = {(0g‘𝑅)} → (𝐸 ↑m 𝑆) = ({(0g‘𝑅)} ↑m 𝑆)) |
| 51 | 50 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝐸 = {(0g‘𝑅)} → (∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)) ↔ ∀𝑓 ∈ ({(0g‘𝑅)} ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)))) |
| 52 | 51 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)) ↔ ∀𝑓 ∈ ({(0g‘𝑅)} ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅)))) |
| 53 | 49, 52 | mpbird 257 |
. . . . . . . 8
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅))) |
| 54 | | simpl 482 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵)) |
| 55 | 54 | ancomd 461 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod)) |
| 56 | 55 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod)) |
| 57 | | lindsrng01.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑀) |
| 58 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 59 | 57, 58, 1, 2, 15 | islininds 48363 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅))))) |
| 60 | 56, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp (0g‘𝑅) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑆 (𝑓‘𝑣) = (0g‘𝑅))))) |
| 61 | 20, 53, 60 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝐸 = {(0g‘𝑅)} ∧ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1)) → 𝑆 linIndS 𝑀) |
| 62 | 17, 61 | mpancom 688 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (♯‘𝐸) = 1) → 𝑆 linIndS 𝑀) |
| 63 | 62 | expcom 413 |
. . . . 5
⊢
((♯‘𝐸) =
1 → ((𝑀 ∈ LMod
∧ 𝑆 ∈ 𝒫
𝐵) → 𝑆 linIndS 𝑀)) |
| 64 | 12, 63 | jaoi 858 |
. . . 4
⊢
(((♯‘𝐸)
= 0 ∨ (♯‘𝐸)
= 1) → ((𝑀 ∈ LMod
∧ 𝑆 ∈ 𝒫
𝐵) → 𝑆 linIndS 𝑀)) |
| 65 | 64 | expd 415 |
. . 3
⊢
(((♯‘𝐸)
= 0 ∨ (♯‘𝐸)
= 1) → (𝑀 ∈ LMod
→ (𝑆 ∈ 𝒫
𝐵 → 𝑆 linIndS 𝑀))) |
| 66 | 65 | com12 32 |
. 2
⊢ (𝑀 ∈ LMod →
(((♯‘𝐸) = 0
∨ (♯‘𝐸) = 1)
→ (𝑆 ∈ 𝒫
𝐵 → 𝑆 linIndS 𝑀))) |
| 67 | 66 | 3imp 1111 |
1
⊢ ((𝑀 ∈ LMod ∧
((♯‘𝐸) = 0 ∨
(♯‘𝐸) = 1)
∧ 𝑆 ∈ 𝒫
𝐵) → 𝑆 linIndS 𝑀) |