| Step | Hyp | Ref
| Expression |
| 1 | | lindsun.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 2 | | lveclmod 21105 |
. . 3
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 4 | | lindsun.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 6 | 5 | linds1 21830 |
. . . 4
⊢ (𝑈 ∈ (LIndS‘𝑊) → 𝑈 ⊆ (Base‘𝑊)) |
| 7 | 4, 6 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑊)) |
| 8 | | lindsun.v |
. . . 4
⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) |
| 9 | 5 | linds1 21830 |
. . . 4
⊢ (𝑉 ∈ (LIndS‘𝑊) → 𝑉 ⊆ (Base‘𝑊)) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝑊)) |
| 11 | 7, 10 | unssd 4192 |
. 2
⊢ (𝜑 → (𝑈 ∪ 𝑉) ⊆ (Base‘𝑊)) |
| 12 | | lindsun.n |
. . . . . . . . . 10
⊢ 𝑁 = (LSpan‘𝑊) |
| 13 | | lindsun.0 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑊) |
| 14 | 1 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → 𝑊 ∈ LVec) |
| 15 | 4 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → 𝑈 ∈ (LIndS‘𝑊)) |
| 16 | 8 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → 𝑉 ∈ (LIndS‘𝑊)) |
| 17 | | lindsun.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) |
| 18 | 17 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) |
| 19 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
| 20 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 21 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ 𝑈) |
| 22 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) |
| 23 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) |
| 24 | 12, 13, 14, 15, 16, 18, 19, 20, 21, 22, 23 | lindsunlem 33675 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑈) → ⊥) |
| 25 | 24 | adantlr 715 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) ∧ 𝑐 ∈ 𝑈) → ⊥) |
| 26 | 1 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → 𝑊 ∈ LVec) |
| 27 | 8 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → 𝑉 ∈ (LIndS‘𝑊)) |
| 28 | 4 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → 𝑈 ∈ (LIndS‘𝑊)) |
| 29 | | incom 4209 |
. . . . . . . . . . . 12
⊢ ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = ((𝑁‘𝑉) ∩ (𝑁‘𝑈)) |
| 30 | 29, 17 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁‘𝑉) ∩ (𝑁‘𝑈)) = { 0 }) |
| 31 | 30 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → ((𝑁‘𝑉) ∩ (𝑁‘𝑈)) = { 0 }) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉) |
| 33 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) |
| 34 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) |
| 35 | | uncom 4158 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∪ 𝑉) = (𝑉 ∪ 𝑈) |
| 36 | 35 | difeq1i 4122 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∪ 𝑉) ∖ {𝑐}) = ((𝑉 ∪ 𝑈) ∖ {𝑐}) |
| 37 | 36 | fveq2i 6909 |
. . . . . . . . . . 11
⊢ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐})) = (𝑁‘((𝑉 ∪ 𝑈) ∖ {𝑐})) |
| 38 | 34, 37 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑉 ∪ 𝑈) ∖ {𝑐}))) |
| 39 | 12, 13, 26, 27, 28, 31, 19, 20, 32, 33, 38 | lindsunlem 33675 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ 𝑉) → ⊥) |
| 40 | 39 | adantlr 715 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) ∧ 𝑐 ∈ 𝑉) → ⊥) |
| 41 | | elun 4153 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (𝑈 ∪ 𝑉) ↔ (𝑐 ∈ 𝑈 ∨ 𝑐 ∈ 𝑉)) |
| 42 | 41 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑐 ∈ (𝑈 ∪ 𝑉) → (𝑐 ∈ 𝑈 ∨ 𝑐 ∈ 𝑉)) |
| 43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) → (𝑐 ∈ 𝑈 ∨ 𝑐 ∈ 𝑉)) |
| 44 | 25, 40, 43 | mpjaodan 961 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) → ⊥) |
| 45 | 44 | an32s 652 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) ∧ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) → ⊥) |
| 46 | 45 | inegd 1560 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) → ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) |
| 47 | 46 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑐 ∈ (𝑈 ∪ 𝑉)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) |
| 48 | 47 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑐 ∈ (𝑈 ∪ 𝑉) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) |
| 49 | 48 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ (𝑈 ∪ 𝑉)∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))) |
| 50 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 51 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 52 | 5, 50, 12, 51, 20, 19 | islinds2 21833 |
. . 3
⊢ (𝑊 ∈ LMod → ((𝑈 ∪ 𝑉) ∈ (LIndS‘𝑊) ↔ ((𝑈 ∪ 𝑉) ⊆ (Base‘𝑊) ∧ ∀𝑐 ∈ (𝑈 ∪ 𝑉)∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐}))))) |
| 53 | 52 | biimpar 477 |
. 2
⊢ ((𝑊 ∈ LMod ∧ ((𝑈 ∪ 𝑉) ⊆ (Base‘𝑊) ∧ ∀𝑐 ∈ (𝑈 ∪ 𝑉)∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑐) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝑐})))) → (𝑈 ∪ 𝑉) ∈ (LIndS‘𝑊)) |
| 54 | 3, 11, 49, 53 | syl12anc 837 |
1
⊢ (𝜑 → (𝑈 ∪ 𝑉) ∈ (LIndS‘𝑊)) |