| 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 38992 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}))) |
| 8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}))) |
| 9 | 1, 8 | mpbid 232 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤})) |
| 10 | | lsatfixed.p |
. . . . 5
⊢ + =
(+g‘𝑊) |
| 11 | 2 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑊 ∈ LVec) |
| 12 | | lsatfixed.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 13 | 12 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑋 ∈ 𝑉) |
| 14 | | lsatfixed.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑌 ∈ 𝑉) |
| 16 | | simp2 1138 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
| 17 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 = (𝑁‘{𝑤})) |
| 18 | 17 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) = 𝑄) |
| 19 | | lsatfixed.e |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋})) |
| 20 | 19 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ≠ (𝑁‘{𝑋})) |
| 21 | 18, 20 | eqnetrd 3008 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋})) |
| 22 | 3, 5, 4, 11, 16, 13, 21 | lspsnne1 21119 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ¬ 𝑤 ∈ (𝑁‘{𝑋})) |
| 23 | | lsatfixed.f |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌})) |
| 24 | 23 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ≠ (𝑁‘{𝑌})) |
| 25 | 18, 24 | eqnetrd 3008 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌})) |
| 26 | 3, 5, 4, 11, 16, 15, 25 | lspsnne1 21119 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ¬ 𝑤 ∈ (𝑁‘{𝑌})) |
| 27 | | lsatfixed.g |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) |
| 28 | 27 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) |
| 29 | 18, 28 | eqsstrd 4018 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ⊆ (𝑁‘{𝑋, 𝑌})) |
| 30 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 31 | | lveclmod 21105 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 32 | 2, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 33 | 32 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑊 ∈ LMod) |
| 34 | 3, 30, 4, 32, 12, 14 | lspprcl 20976 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑊)) |
| 35 | 34 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑊)) |
| 36 | 16 | eldifad 3963 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ 𝑉) |
| 37 | 3, 30, 4, 33, 35, 36 | ellspsn5b 20993 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (𝑤 ∈ (𝑁‘{𝑋, 𝑌}) ↔ (𝑁‘{𝑤}) ⊆ (𝑁‘{𝑋, 𝑌}))) |
| 38 | 29, 37 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
| 39 | 3, 10, 5, 4, 11, 13, 15, 22, 26, 38 | lspfixed 21130 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)})) |
| 40 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝜑) |
| 41 | 40, 2 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑊 ∈ LVec) |
| 42 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
| 43 | 40, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑊 ∈ LMod) |
| 44 | 40, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑋 ∈ 𝑉) |
| 45 | 14 | snssd 4809 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑌} ⊆ 𝑉) |
| 46 | 3, 4 | lspssv 20981 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ {𝑌} ⊆ 𝑉) → (𝑁‘{𝑌}) ⊆ 𝑉) |
| 47 | 32, 45, 46 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉) |
| 48 | 47 | ssdifssd 4147 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁‘{𝑌}) ∖ { 0 }) ⊆ 𝑉) |
| 49 | 48 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ((𝑁‘{𝑌}) ∖ { 0 }) ⊆ 𝑉) |
| 50 | 49 | sselda 3983 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑧 ∈ 𝑉) |
| 51 | 3, 10 | lmodvacl 20873 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑋 + 𝑧) ∈ 𝑉) |
| 52 | 43, 44, 50, 51 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑋 + 𝑧) ∈ 𝑉) |
| 53 | 3, 5, 4, 41, 42, 52 | lspsncmp 21118 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → ((𝑁‘{𝑤}) ⊆ (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) = (𝑁‘{(𝑋 + 𝑧)}))) |
| 54 | 3, 30, 4 | lspsncl 20975 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑧) ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑧)}) ∈ (LSubSp‘𝑊)) |
| 55 | 43, 52, 54 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑁‘{(𝑋 + 𝑧)}) ∈ (LSubSp‘𝑊)) |
| 56 | 42 | eldifad 3963 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑤 ∈ 𝑉) |
| 57 | 3, 30, 4, 43, 55, 56 | ellspsn5b 20993 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) ⊆ (𝑁‘{(𝑋 + 𝑧)}))) |
| 58 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → 𝑄 = (𝑁‘{𝑤})) |
| 59 | 58 | eqeq1d 2739 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ (𝑁‘{𝑤}) = (𝑁‘{(𝑋 + 𝑧)}))) |
| 60 | 53, 57, 59 | 3bitr4rd 312 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) ∧ 𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })) → (𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ 𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}))) |
| 61 | 60 | rexbidva 3177 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → (∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}) ↔ ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑤 ∈ (𝑁‘{(𝑋 + 𝑧)}))) |
| 62 | 39, 61 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑉 ∖ { 0 }) ∧ 𝑄 = (𝑁‘{𝑤})) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) |
| 63 | 62 | rexlimdv3a 3159 |
. 2
⊢ (𝜑 → (∃𝑤 ∈ (𝑉 ∖ { 0 })𝑄 = (𝑁‘{𝑤}) → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}))) |
| 64 | 9, 63 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) |