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 34278 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}))) |
8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}))) |
9 | 1, 8 | mpbid 222 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤})) |
10 | | lsatfixed.p |
. . . . 5
⊢ + =
(+g‘𝑊) |
11 | 2 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑊 ∈ LVec) |
12 | | simp2 1062 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
13 | 12 | eldifad 3586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ 𝑉) |
14 | | lsatfixed.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
15 | 14 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑋 ∈ 𝑉) |
16 | | lsatfixed.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
17 | 16 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑌 ∈ 𝑉) |
18 | | simp3 1063 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 = (𝑁‘{𝑤})) |
19 | 18 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) = 𝑄) |
20 | | lsatfixed.e |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋})) |
21 | 20 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ≠ (𝑁‘{𝑋})) |
22 | 19, 21 | eqnetrd 2861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋})) |
23 | 3, 5, 4, 11, 12, 15, 22 | lspsnne1 19117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ¬ 𝑤 ∈ (𝑁‘{𝑋})) |
24 | | lsatfixed.f |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌})) |
25 | 24 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ≠ (𝑁‘{𝑌})) |
26 | 19, 25 | eqnetrd 2861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌})) |
27 | 3, 5, 4, 11, 12, 17, 26 | lspsnne1 19117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ¬ 𝑤 ∈ (𝑁‘{𝑌})) |
28 | | lsatfixed.g |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) |
29 | 28 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) |
30 | 19, 29 | eqsstrd 3639 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ⊆ (𝑁‘{𝑋, 𝑌})) |
31 | | eqid 2622 |
. . . . . . 7
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
32 | | lveclmod 19106 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
33 | 2, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
34 | 33 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑊 ∈ LMod) |
35 | 3, 31, 4, 33, 14, 16 | lspprcl 18978 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑊)) |
36 | 35 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑊)) |
37 | 3, 31, 4, 34, 36, 13 | lspsnel5 18995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑤 ∈ (𝑁‘{𝑋, 𝑌}) ↔ (𝑁‘{𝑤}) ⊆ (𝑁‘{𝑋, 𝑌}))) |
38 | 30, 37 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
39 | 3, 10, 5, 4, 11, 13, 15, 17, 23, 27, 38 | lspfixed 19128 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)})) |
40 | | simpl1 1064 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝜑) |
41 | 40, 2 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑊 ∈ LVec) |
42 | | simpl2 1065 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
43 | 40, 33 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑊 ∈ LMod) |
44 | 40, 14 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑋 ∈ 𝑉) |
45 | 16 | snssd 4340 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑌} ⊆ 𝑉) |
46 | 3, 4 | lspssv 18983 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ {𝑌} ⊆ 𝑉) → (𝑁‘{𝑌}) ⊆ 𝑉) |
47 | 33, 45, 46 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉) |
48 | 47 | ssdifssd 3748 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁‘{𝑌}) ∖ { 0 }) ⊆ 𝑉) |
49 | 48 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ((𝑁‘{𝑌}) ∖ { 0 }) ⊆ 𝑉) |
50 | 49 | sselda 3603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑧 ∈ 𝑉) |
51 | 3, 10 | lmodvacl 18877 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑋 + 𝑧) ∈ 𝑉) |
52 | 43, 44, 50, 51 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑋 + 𝑧) ∈ 𝑉) |
53 | 3, 5, 4, 41, 42, 52 | lspsncmp 19116 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → ((𝑁‘{𝑤}) ⊆ (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) = (𝑁‘{(𝑋 + 𝑧)}))) |
54 | 3, 31, 4 | lspsncl 18977 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑧) ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑧)}) ∈ (LSubSp‘𝑊)) |
55 | 43, 52, 54 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑁‘{(𝑋 + 𝑧)}) ∈ (LSubSp‘𝑊)) |
56 | 42 | eldifad 3586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑤 ∈ 𝑉) |
57 | 3, 31, 4, 43, 55, 56 | lspsnel5 18995 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) ⊆ (𝑁‘{(𝑋 + 𝑧)}))) |
58 | | simpl3 1066 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑄 = (𝑁‘{𝑤})) |
59 | 58 | eqeq1d 2624 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) = (𝑁‘{(𝑋 + 𝑧)}))) |
60 | 53, 57, 59 | 3bitr4rd 301 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ 𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}))) |
61 | 60 | rexbidva 3049 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}))) |
62 | 39, 61 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) |
63 | 62 | rexlimdv3a 3033 |
. 2
⊢ (𝜑 → (∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}))) |
64 | 9, 63 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) |