Proof of Theorem mapdindp2
Step | Hyp | Ref
| Expression |
1 | | preq2 4269 |
. . . . . 6
⊢ ((𝑌 + 𝑍) = 0 → {𝑋, (𝑌 + 𝑍)} = {𝑋, 0 }) |
2 | 1 | fveq2d 6195 |
. . . . 5
⊢ ((𝑌 + 𝑍) = 0 → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋, 0 })) |
3 | | mapdindp1.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑊) |
4 | | mapdindp1.o |
. . . . . 6
⊢ 0 =
(0g‘𝑊) |
5 | | mapdindp1.n |
. . . . . 6
⊢ 𝑁 = (LSpan‘𝑊) |
6 | | mapdindp1.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LVec) |
7 | | lveclmod 19106 |
. . . . . . 7
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) |
9 | | mapdindp1.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
10 | 9 | eldifad 3586 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
11 | 3, 4, 5, 8, 10 | lsppr0 19092 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋, 0 }) = (𝑁‘{𝑋})) |
12 | 2, 11 | sylan9eqr 2678 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋})) |
13 | | mapdindp1.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
14 | 13 | eldifad 3586 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
15 | | prssi 4353 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉) |
16 | 10, 14, 15 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉) |
17 | | snsspr1 4345 |
. . . . . . 7
⊢ {𝑋} ⊆ {𝑋, 𝑌} |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑋} ⊆ {𝑋, 𝑌}) |
19 | 3, 5 | lspss 18984 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ {𝑋, 𝑌} ⊆ 𝑉 ∧ {𝑋} ⊆ {𝑋, 𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌})) |
20 | 8, 16, 18, 19 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌})) |
21 | 20 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌})) |
22 | 12, 21 | eqsstrd 3639 |
. . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) ⊆ (𝑁‘{𝑋, 𝑌})) |
23 | | mapdindp1.f |
. . . 4
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
24 | 23 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
25 | 22, 24 | ssneldd 3606 |
. 2
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) |
26 | 23 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
27 | | mapdindp1.p |
. . . . . 6
⊢ + =
(+g‘𝑊) |
28 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑊 ∈ LVec) |
29 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 })) |
30 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑌 ∈ (𝑉 ∖ { 0 })) |
31 | | mapdindp1.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
32 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑍 ∈ (𝑉 ∖ { 0 })) |
33 | | mapdindp1.W |
. . . . . . 7
⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) |
34 | 33 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
35 | | mapdindp1.e |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) |
37 | | mapdindp1.ne |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
38 | 37 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
39 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑌 + 𝑍) ≠ 0 ) |
40 | 3, 27, 4, 5, 28, 29, 30, 32, 34, 36, 38, 26, 39 | mapdindp0 37008 |
. . . . 5
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌})) |
41 | 40 | oveq2d 6666 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
42 | | eqid 2622 |
. . . . . 6
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) |
43 | 31 | eldifad 3586 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
44 | 3, 27 | lmodvacl 18877 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉) |
45 | 8, 14, 43, 44 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉) |
46 | 3, 5, 42, 8, 10, 45 | lsmpr 19089 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)}))) |
47 | 46 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)}))) |
48 | 3, 5, 42, 8, 10, 14 | lsmpr 19089 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
49 | 48 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
50 | 41, 47, 49 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋, 𝑌})) |
51 | 26, 50 | neleqtrrd 2723 |
. 2
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) |
52 | 25, 51 | pm2.61dane 2881 |
1
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) |