| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) |
| 2 | | lindsun.w |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 3 | | lveclmod 21105 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 5 | | lmodgrp 20865 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ Grp) |
| 7 | 6 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑊 ∈ Grp) |
| 8 | | lmodabl 20907 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
| 9 | 4, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑊 ∈ Abel) |
| 10 | 9 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑊 ∈ Abel) |
| 11 | | lindsun.u |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 13 | 12 | linds1 21830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ (LIndS‘𝑊) → 𝑈 ⊆ (Base‘𝑊)) |
| 14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑊)) |
| 15 | | lindsun.n |
. . . . . . . . . . . . . . . . 17
⊢ 𝑁 = (LSpan‘𝑊) |
| 16 | 12, 15 | lspssv 20981 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ (Base‘𝑊)) → (𝑁‘𝑈) ⊆ (Base‘𝑊)) |
| 17 | 4, 14, 16 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘𝑈) ⊆ (Base‘𝑊)) |
| 18 | 17 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑁‘𝑈) ⊆ (Base‘𝑊)) |
| 19 | | difssd 4137 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 ∖ {𝐶}) ⊆ 𝑈) |
| 20 | 12, 15 | lspss 20982 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ (Base‘𝑊) ∧ (𝑈 ∖ {𝐶}) ⊆ 𝑈) → (𝑁‘(𝑈 ∖ {𝐶})) ⊆ (𝑁‘𝑈)) |
| 21 | 4, 14, 19, 20 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁‘(𝑈 ∖ {𝐶})) ⊆ (𝑁‘𝑈)) |
| 22 | 21 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑁‘(𝑈 ∖ {𝐶})) ⊆ (𝑁‘𝑈)) |
| 23 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) |
| 24 | 22, 23 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑥 ∈ (𝑁‘𝑈)) |
| 25 | 18, 24 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑥 ∈ (Base‘𝑊)) |
| 26 | | lindsun.v |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) |
| 27 | 12 | linds1 21830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ (LIndS‘𝑊) → 𝑉 ⊆ (Base‘𝑊)) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝑊)) |
| 29 | 12, 15 | lspssv 20981 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
| 30 | 4, 28, 29 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
| 31 | 30 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
| 32 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑦 ∈ (𝑁‘𝑉)) |
| 33 | 31, 32 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑦 ∈ (Base‘𝑊)) |
| 34 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 35 | 12, 34 | ablcom 19817 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Abel ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(+g‘𝑊)𝑦) = (𝑦(+g‘𝑊)𝑥)) |
| 36 | 10, 25, 33, 35 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑥(+g‘𝑊)𝑦) = (𝑦(+g‘𝑊)𝑥)) |
| 37 | 1, 36 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑦(+g‘𝑊)𝑥) = (𝐾( ·𝑠
‘𝑊)𝐶)) |
| 38 | | lindsunlem.k |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) |
| 39 | 38 | eldifad 3963 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ 𝐹) |
| 40 | | lindsunlem.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
| 41 | 14, 40 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ (Base‘𝑊)) |
| 42 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 43 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 44 | | lindsunlem.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 =
(Base‘(Scalar‘𝑊)) |
| 45 | 12, 42, 43, 44 | lmodvscl 20876 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝐾 ∈ 𝐹 ∧ 𝐶 ∈ (Base‘𝑊)) → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (Base‘𝑊)) |
| 46 | 4, 39, 41, 45 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (Base‘𝑊)) |
| 47 | 46 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (Base‘𝑊)) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(-g‘𝑊) = (-g‘𝑊) |
| 49 | 12, 34, 48 | grpsubadd 19046 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Grp ∧ ((𝐾(
·𝑠 ‘𝑊)𝐶) ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (((𝐾( ·𝑠
‘𝑊)𝐶)(-g‘𝑊)𝑥) = 𝑦 ↔ (𝑦(+g‘𝑊)𝑥) = (𝐾( ·𝑠
‘𝑊)𝐶))) |
| 50 | 49 | biimpar 477 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Grp ∧ ((𝐾(
·𝑠 ‘𝑊)𝐶) ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑦(+g‘𝑊)𝑥) = (𝐾( ·𝑠
‘𝑊)𝐶)) → ((𝐾( ·𝑠
‘𝑊)𝐶)(-g‘𝑊)𝑥) = 𝑦) |
| 51 | 50 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Grp ∧ (𝑦(+g‘𝑊)𝑥) = (𝐾( ·𝑠
‘𝑊)𝐶)) ∧ ((𝐾( ·𝑠
‘𝑊)𝐶) ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝐾( ·𝑠
‘𝑊)𝐶)(-g‘𝑊)𝑥) = 𝑦) |
| 52 | 7, 37, 47, 25, 33, 51 | syl23anc 1379 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → ((𝐾( ·𝑠
‘𝑊)𝐶)(-g‘𝑊)𝑥) = 𝑦) |
| 53 | 4 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑊 ∈ LMod) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 55 | 12, 54, 15 | lspcl 20974 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ (Base‘𝑊)) → (𝑁‘𝑈) ∈ (LSubSp‘𝑊)) |
| 56 | 4, 14, 55 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘𝑈) ∈ (LSubSp‘𝑊)) |
| 57 | 56 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑁‘𝑈) ∈ (LSubSp‘𝑊)) |
| 58 | 39 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝐾 ∈ 𝐹) |
| 59 | 12, 15 | lspssid 20983 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ (Base‘𝑊)) → 𝑈 ⊆ (𝑁‘𝑈)) |
| 60 | 4, 14, 59 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈)) |
| 61 | 60, 40 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ (𝑁‘𝑈)) |
| 62 | 61 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝐶 ∈ (𝑁‘𝑈)) |
| 63 | 42, 43, 44, 54 | lssvscl 20953 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘𝑈) ∈ (LSubSp‘𝑊)) ∧ (𝐾 ∈ 𝐹 ∧ 𝐶 ∈ (𝑁‘𝑈))) → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘𝑈)) |
| 64 | 53, 57, 58, 62, 63 | syl22anc 839 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘𝑈)) |
| 65 | 48, 54 | lssvsubcl 20942 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘𝑈) ∈ (LSubSp‘𝑊)) ∧ ((𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘𝑈) ∧ 𝑥 ∈ (𝑁‘𝑈))) → ((𝐾( ·𝑠
‘𝑊)𝐶)(-g‘𝑊)𝑥) ∈ (𝑁‘𝑈)) |
| 66 | 53, 57, 64, 24, 65 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → ((𝐾( ·𝑠
‘𝑊)𝐶)(-g‘𝑊)𝑥) ∈ (𝑁‘𝑈)) |
| 67 | 52, 66 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑦 ∈ (𝑁‘𝑈)) |
| 68 | 67, 32 | elind 4200 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑦 ∈ ((𝑁‘𝑈) ∩ (𝑁‘𝑉))) |
| 69 | | lindsun.2 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) |
| 70 | 69 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) |
| 71 | 68, 70 | eleqtrd 2843 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑦 ∈ { 0 }) |
| 72 | | elsni 4643 |
. . . . . . 7
⊢ (𝑦 ∈ { 0 } → 𝑦 = 0 ) |
| 73 | 71, 72 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑦 = 0 ) |
| 74 | 73 | oveq2d 7447 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑥(+g‘𝑊)𝑦) = (𝑥(+g‘𝑊) 0 )) |
| 75 | | lindsun.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑊) |
| 76 | 12, 34, 75 | grprid 18986 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(+g‘𝑊) 0 ) = 𝑥) |
| 77 | 7, 25, 76 | syl2anc 584 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝑥(+g‘𝑊) 0 ) = 𝑥) |
| 78 | 1, 74, 77 | 3eqtrd 2781 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝐾( ·𝑠
‘𝑊)𝐶) = 𝑥) |
| 79 | 78, 23 | eqeltrd 2841 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶}))) |
| 80 | 40 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝐶 ∈ 𝑈) |
| 81 | 38 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝐾 ∈ (𝐹 ∖ {𝑂})) |
| 82 | 2 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑊 ∈ LVec) |
| 83 | 11 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → 𝑈 ∈ (LIndS‘𝑊)) |
| 84 | | lindsunlem.o |
. . . . . . 7
⊢ 𝑂 =
(0g‘(Scalar‘𝑊)) |
| 85 | 12, 43, 15, 42, 44, 84 | islinds2 21833 |
. . . . . 6
⊢ (𝑊 ∈ LVec → (𝑈 ∈ (LIndS‘𝑊) ↔ (𝑈 ⊆ (Base‘𝑊) ∧ ∀𝑐 ∈ 𝑈 ∀𝑘 ∈ (𝐹 ∖ {𝑂}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘(𝑈 ∖ {𝑐}))))) |
| 86 | 85 | simplbda 499 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LIndS‘𝑊)) → ∀𝑐 ∈ 𝑈 ∀𝑘 ∈ (𝐹 ∖ {𝑂}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘(𝑈 ∖ {𝑐}))) |
| 87 | 82, 83, 86 | syl2anc 584 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → ∀𝑐 ∈ 𝑈 ∀𝑘 ∈ (𝐹 ∖ {𝑂}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘(𝑈 ∖ {𝑐}))) |
| 88 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑘( ·𝑠
‘𝑊)𝑐) = (𝑘( ·𝑠
‘𝑊)𝐶)) |
| 89 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → {𝑐} = {𝐶}) |
| 90 | 89 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑈 ∖ {𝑐}) = (𝑈 ∖ {𝐶})) |
| 91 | 90 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑁‘(𝑈 ∖ {𝑐})) = (𝑁‘(𝑈 ∖ {𝐶}))) |
| 92 | 88, 91 | eleq12d 2835 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘(𝑈 ∖ {𝑐})) ↔ (𝑘( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶})))) |
| 93 | 92 | notbid 318 |
. . . . 5
⊢ (𝑐 = 𝐶 → (¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘(𝑈 ∖ {𝑐})) ↔ ¬ (𝑘( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶})))) |
| 94 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑘( ·𝑠
‘𝑊)𝐶) = (𝐾( ·𝑠
‘𝑊)𝐶)) |
| 95 | 94 | eleq1d 2826 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((𝑘( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶})) ↔ (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶})))) |
| 96 | 95 | notbid 318 |
. . . . 5
⊢ (𝑘 = 𝐾 → (¬ (𝑘( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶})) ↔ ¬ (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶})))) |
| 97 | 93, 96 | rspc2va 3634 |
. . . 4
⊢ (((𝐶 ∈ 𝑈 ∧ 𝐾 ∈ (𝐹 ∖ {𝑂})) ∧ ∀𝑐 ∈ 𝑈 ∀𝑘 ∈ (𝐹 ∖ {𝑂}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘(𝑈 ∖ {𝑐}))) → ¬ (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶}))) |
| 98 | 80, 81, 87, 97 | syl21anc 838 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → ¬ (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘(𝑈 ∖ {𝐶}))) |
| 99 | 79, 98 | pm2.21fal 1562 |
. 2
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))) ∧ 𝑦 ∈ (𝑁‘𝑉)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) → ⊥) |
| 100 | 14 | ssdifssd 4147 |
. . . . 5
⊢ (𝜑 → (𝑈 ∖ {𝐶}) ⊆ (Base‘𝑊)) |
| 101 | 12, 54, 15 | lspcl 20974 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ∖ {𝐶}) ⊆ (Base‘𝑊)) → (𝑁‘(𝑈 ∖ {𝐶})) ∈ (LSubSp‘𝑊)) |
| 102 | 4, 100, 101 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑁‘(𝑈 ∖ {𝐶})) ∈ (LSubSp‘𝑊)) |
| 103 | 54 | lsssubg 20955 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘(𝑈 ∖ {𝐶})) ∈ (LSubSp‘𝑊)) → (𝑁‘(𝑈 ∖ {𝐶})) ∈ (SubGrp‘𝑊)) |
| 104 | 4, 102, 103 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑁‘(𝑈 ∖ {𝐶})) ∈ (SubGrp‘𝑊)) |
| 105 | 12, 54, 15 | lspcl 20974 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → (𝑁‘𝑉) ∈ (LSubSp‘𝑊)) |
| 106 | 4, 28, 105 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑁‘𝑉) ∈ (LSubSp‘𝑊)) |
| 107 | 54 | lsssubg 20955 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘𝑉) ∈ (LSubSp‘𝑊)) → (𝑁‘𝑉) ∈ (SubGrp‘𝑊)) |
| 108 | 4, 106, 107 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑁‘𝑉) ∈ (SubGrp‘𝑊)) |
| 109 | | lindsunlem.1 |
. . . 4
⊢ (𝜑 → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) |
| 110 | | eqid 2737 |
. . . . . . 7
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) |
| 111 | 12, 15, 110 | lsmsp2 21086 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ∖ {𝐶}) ⊆ (Base‘𝑊) ∧ 𝑉 ⊆ (Base‘𝑊)) → ((𝑁‘(𝑈 ∖ {𝐶}))(LSSum‘𝑊)(𝑁‘𝑉)) = (𝑁‘((𝑈 ∖ {𝐶}) ∪ 𝑉))) |
| 112 | 4, 100, 28, 111 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝑁‘(𝑈 ∖ {𝐶}))(LSSum‘𝑊)(𝑁‘𝑉)) = (𝑁‘((𝑈 ∖ {𝐶}) ∪ 𝑉))) |
| 113 | 61 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ (𝑁‘𝑈)) |
| 114 | 12, 15 | lspssid 20983 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → 𝑉 ⊆ (𝑁‘𝑉)) |
| 115 | 4, 28, 114 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ⊆ (𝑁‘𝑉)) |
| 116 | 115 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ (𝑁‘𝑉)) |
| 117 | 113, 116 | elind 4200 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ((𝑁‘𝑈) ∩ (𝑁‘𝑉))) |
| 118 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) |
| 119 | 117, 118 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ { 0 }) |
| 120 | | elsni 4643 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ { 0 } → 𝐶 = 0 ) |
| 121 | 119, 120 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → 𝐶 = 0 ) |
| 122 | 75 | 0nellinds 33398 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝑈) |
| 123 | 2, 11, 122 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 0 ∈ 𝑈) |
| 124 | | nelne2 3040 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ 𝑈 ∧ ¬ 0 ∈ 𝑈) → 𝐶 ≠ 0 ) |
| 125 | 40, 123, 124 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ≠ 0 ) |
| 126 | 125 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → 𝐶 ≠ 0 ) |
| 127 | 126 | neneqd 2945 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → ¬ 𝐶 = 0 ) |
| 128 | 121, 127 | pm2.65da 817 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝐶 ∈ 𝑉) |
| 129 | | disjsn 4711 |
. . . . . . . . 9
⊢ ((𝑉 ∩ {𝐶}) = ∅ ↔ ¬ 𝐶 ∈ 𝑉) |
| 130 | 128, 129 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → (𝑉 ∩ {𝐶}) = ∅) |
| 131 | | undif4 4467 |
. . . . . . . 8
⊢ ((𝑉 ∩ {𝐶}) = ∅ → (𝑉 ∪ (𝑈 ∖ {𝐶})) = ((𝑉 ∪ 𝑈) ∖ {𝐶})) |
| 132 | 130, 131 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑉 ∪ (𝑈 ∖ {𝐶})) = ((𝑉 ∪ 𝑈) ∖ {𝐶})) |
| 133 | | uncom 4158 |
. . . . . . 7
⊢ ((𝑈 ∖ {𝐶}) ∪ 𝑉) = (𝑉 ∪ (𝑈 ∖ {𝐶})) |
| 134 | | uncom 4158 |
. . . . . . . 8
⊢ (𝑈 ∪ 𝑉) = (𝑉 ∪ 𝑈) |
| 135 | 134 | difeq1i 4122 |
. . . . . . 7
⊢ ((𝑈 ∪ 𝑉) ∖ {𝐶}) = ((𝑉 ∪ 𝑈) ∖ {𝐶}) |
| 136 | 132, 133,
135 | 3eqtr4g 2802 |
. . . . . 6
⊢ (𝜑 → ((𝑈 ∖ {𝐶}) ∪ 𝑉) = ((𝑈 ∪ 𝑉) ∖ {𝐶})) |
| 137 | 136 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (𝑁‘((𝑈 ∖ {𝐶}) ∪ 𝑉)) = (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) |
| 138 | 112, 137 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((𝑁‘(𝑈 ∖ {𝐶}))(LSSum‘𝑊)(𝑁‘𝑉)) = (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) |
| 139 | 109, 138 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → (𝐾( ·𝑠
‘𝑊)𝐶) ∈ ((𝑁‘(𝑈 ∖ {𝐶}))(LSSum‘𝑊)(𝑁‘𝑉))) |
| 140 | 34, 110 | lsmelval 19667 |
. . . 4
⊢ (((𝑁‘(𝑈 ∖ {𝐶})) ∈ (SubGrp‘𝑊) ∧ (𝑁‘𝑉) ∈ (SubGrp‘𝑊)) → ((𝐾( ·𝑠
‘𝑊)𝐶) ∈ ((𝑁‘(𝑈 ∖ {𝐶}))(LSSum‘𝑊)(𝑁‘𝑉)) ↔ ∃𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))∃𝑦 ∈ (𝑁‘𝑉)(𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦))) |
| 141 | 140 | biimpa 476 |
. . 3
⊢ ((((𝑁‘(𝑈 ∖ {𝐶})) ∈ (SubGrp‘𝑊) ∧ (𝑁‘𝑉) ∈ (SubGrp‘𝑊)) ∧ (𝐾( ·𝑠
‘𝑊)𝐶) ∈ ((𝑁‘(𝑈 ∖ {𝐶}))(LSSum‘𝑊)(𝑁‘𝑉))) → ∃𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))∃𝑦 ∈ (𝑁‘𝑉)(𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) |
| 142 | 104, 108,
139, 141 | syl21anc 838 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ (𝑁‘(𝑈 ∖ {𝐶}))∃𝑦 ∈ (𝑁‘𝑉)(𝐾( ·𝑠
‘𝑊)𝐶) = (𝑥(+g‘𝑊)𝑦)) |
| 143 | 99, 142 | r19.29vva 3216 |
1
⊢ (𝜑 → ⊥) |