Step | Hyp | Ref
| Expression |
1 | | lsatfixed.q |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
2 | | lsatfixed.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LVec) |
3 | | lsatfixed.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
4 | | lsatfixed.n |
. . . . 5
⊢ 𝑁 = (LSpan‘𝑊) |
5 | | lsatfixed.o |
. . . . 5
⊢ 0 =
(0g‘𝑊) |
6 | | lsatfixed.a |
. . . . 5
⊢ 𝐴 = (LSAtoms‘𝑊) |
7 | 3, 4, 5, 6 | islsat 37005 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}))) |
8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}))) |
9 | 1, 8 | mpbid 231 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤})) |
10 | | lsatfixed.p |
. . . . 5
⊢ + =
(+g‘𝑊) |
11 | 2 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑊 ∈ LVec) |
12 | | lsatfixed.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
13 | 12 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑋 ∈ 𝑉) |
14 | | lsatfixed.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
15 | 14 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑌 ∈ 𝑉) |
16 | | simp2 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
17 | | simp3 1137 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 = (𝑁‘{𝑤})) |
18 | 17 | eqcomd 2744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) = 𝑄) |
19 | | lsatfixed.e |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋})) |
20 | 19 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ≠ (𝑁‘{𝑋})) |
21 | 18, 20 | eqnetrd 3011 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋})) |
22 | 3, 5, 4, 11, 16, 13, 21 | lspsnne1 20379 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ¬ 𝑤 ∈ (𝑁‘{𝑋})) |
23 | | lsatfixed.f |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌})) |
24 | 23 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ≠ (𝑁‘{𝑌})) |
25 | 18, 24 | eqnetrd 3011 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌})) |
26 | 3, 5, 4, 11, 16, 15, 25 | lspsnne1 20379 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ¬ 𝑤 ∈ (𝑁‘{𝑌})) |
27 | | lsatfixed.g |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) |
28 | 27 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) |
29 | 18, 28 | eqsstrd 3959 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ⊆ (𝑁‘{𝑋, 𝑌})) |
30 | | eqid 2738 |
. . . . . . 7
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
31 | | lveclmod 20368 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
32 | 2, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
33 | 32 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑊 ∈ LMod) |
34 | 3, 30, 4, 32, 12, 14 | lspprcl 20240 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑊)) |
35 | 34 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑊)) |
36 | 16 | eldifad 3899 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ 𝑉) |
37 | 3, 30, 4, 33, 35, 36 | lspsnel5 20257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑤 ∈ (𝑁‘{𝑋, 𝑌}) ↔ (𝑁‘{𝑤}) ⊆ (𝑁‘{𝑋, 𝑌}))) |
38 | 29, 37 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
39 | 3, 10, 5, 4, 11, 13, 15, 22, 26, 38 | lspfixed 20390 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)})) |
40 | | simpl1 1190 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝜑) |
41 | 40, 2 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑊 ∈ LVec) |
42 | | simpl2 1191 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
43 | 40, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑊 ∈ LMod) |
44 | 40, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑋 ∈ 𝑉) |
45 | 14 | snssd 4742 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑌} ⊆ 𝑉) |
46 | 3, 4 | lspssv 20245 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ {𝑌} ⊆ 𝑉) → (𝑁‘{𝑌}) ⊆ 𝑉) |
47 | 32, 45, 46 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉) |
48 | 47 | ssdifssd 4077 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁‘{𝑌}) ∖ { 0 }) ⊆ 𝑉) |
49 | 48 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ((𝑁‘{𝑌}) ∖ { 0 }) ⊆ 𝑉) |
50 | 49 | sselda 3921 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑧 ∈ 𝑉) |
51 | 3, 10 | lmodvacl 20137 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑋 + 𝑧) ∈ 𝑉) |
52 | 43, 44, 50, 51 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑋 + 𝑧) ∈ 𝑉) |
53 | 3, 5, 4, 41, 42, 52 | lspsncmp 20378 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → ((𝑁‘{𝑤}) ⊆ (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) = (𝑁‘{(𝑋 + 𝑧)}))) |
54 | 3, 30, 4 | lspsncl 20239 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑧) ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑧)}) ∈ (LSubSp‘𝑊)) |
55 | 43, 52, 54 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑁‘{(𝑋 + 𝑧)}) ∈ (LSubSp‘𝑊)) |
56 | 42 | eldifad 3899 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑤 ∈ 𝑉) |
57 | 3, 30, 4, 43, 55, 56 | lspsnel5 20257 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) ⊆ (𝑁‘{(𝑋 + 𝑧)}))) |
58 | | simpl3 1192 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑄 = (𝑁‘{𝑤})) |
59 | 58 | eqeq1d 2740 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) = (𝑁‘{(𝑋 + 𝑧)}))) |
60 | 53, 57, 59 | 3bitr4rd 312 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ 𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}))) |
61 | 60 | rexbidva 3225 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}))) |
62 | 39, 61 | mpbird 256 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) |
63 | 62 | rexlimdv3a 3215 |
. 2
⊢ (𝜑 → (∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}))) |
64 | 9, 63 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) |