| Step | Hyp | Ref
| Expression |
| 1 | | baerlem3.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
| 2 | | baerlem3.p |
. . . . . . 7
⊢ + =
(+g‘𝑊) |
| 3 | | baerlem3.m |
. . . . . . 7
⊢ − =
(-g‘𝑊) |
| 4 | | baerlem3.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 5 | | lveclmod 21105 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 7 | | lmodabl 20907 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
| 8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Abel) |
| 9 | | baerlem3.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 10 | | baerlem3.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
| 11 | 10 | eldifad 3963 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 12 | | baerlem3.z |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
| 13 | 12 | eldifad 3963 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
| 14 | 1, 2, 3, 8, 9, 11,
13 | ablsubsub4 19836 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) |
| 15 | 14 | sneqd 4638 |
. . . . 5
⊢ (𝜑 → {((𝑋 − 𝑌) − 𝑍)} = {(𝑋 − (𝑌 + 𝑍))}) |
| 16 | 15 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝑁‘{((𝑋 − 𝑌) − 𝑍)}) = (𝑁‘{(𝑋 − (𝑌 + 𝑍))})) |
| 17 | 1, 3 | lmodvsubcl 20905 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉) |
| 18 | 6, 9, 11, 17 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑉) |
| 19 | | baerlem3.s |
. . . . . 6
⊢ ⊕ =
(LSSum‘𝑊) |
| 20 | | baerlem3.n |
. . . . . 6
⊢ 𝑁 = (LSpan‘𝑊) |
| 21 | 1, 3, 19, 20 | lspsntrim 21097 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑋 − 𝑌) ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑁‘{((𝑋 − 𝑌) − 𝑍)}) ⊆ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍}))) |
| 22 | 6, 18, 13, 21 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑁‘{((𝑋 − 𝑌) − 𝑍)}) ⊆ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍}))) |
| 23 | 16, 22 | eqsstrrd 4019 |
. . 3
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊆ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍}))) |
| 24 | 1, 3, 8, 9, 13, 11 | ablsub32 19839 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − 𝑍) − 𝑌) = ((𝑋 − 𝑌) − 𝑍)) |
| 25 | 24, 14 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − 𝑍) − 𝑌) = (𝑋 − (𝑌 + 𝑍))) |
| 26 | 25 | sneqd 4638 |
. . . . 5
⊢ (𝜑 → {((𝑋 − 𝑍) − 𝑌)} = {(𝑋 − (𝑌 + 𝑍))}) |
| 27 | 26 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝑁‘{((𝑋 − 𝑍) − 𝑌)}) = (𝑁‘{(𝑋 − (𝑌 + 𝑍))})) |
| 28 | 1, 3 | lmodvsubcl 20905 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑋 − 𝑍) ∈ 𝑉) |
| 29 | 6, 9, 13, 28 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑋 − 𝑍) ∈ 𝑉) |
| 30 | 1, 3, 19, 20 | lspsntrim 21097 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑋 − 𝑍) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{((𝑋 − 𝑍) − 𝑌)}) ⊆ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) |
| 31 | 6, 29, 11, 30 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑁‘{((𝑋 − 𝑍) − 𝑌)}) ⊆ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) |
| 32 | 27, 31 | eqsstrrd 4019 |
. . 3
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊆ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) |
| 33 | 23, 32 | ssind 4241 |
. 2
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊆ (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})))) |
| 34 | | elin 3967 |
. . . . 5
⊢ (𝑗 ∈ (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) ↔ (𝑗 ∈ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∧ 𝑗 ∈ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})))) |
| 35 | | baerlem3.r |
. . . . . . 7
⊢ 𝑅 = (Scalar‘𝑊) |
| 36 | | baerlem3.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 37 | | baerlem3.t |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
| 38 | 1, 2, 35, 36, 37, 19, 20, 6, 18, 13 | lsmspsn 21083 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ↔ ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)))) |
| 39 | 1, 2, 35, 36, 37, 19, 20, 6, 29, 11 | lsmspsn 21083 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})) ↔ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌)))) |
| 40 | 38, 39 | anbi12d 632 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∧ 𝑗 ∈ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) ↔ (∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)) ∧ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))))) |
| 41 | 34, 40 | bitrid 283 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) ↔ (∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)) ∧ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))))) |
| 42 | | baerlem3.o |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑊) |
| 43 | | simp11 1204 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝜑) |
| 44 | 43, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑊 ∈ LVec) |
| 45 | 43, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑋 ∈ 𝑉) |
| 46 | | baerlem3.c |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
| 47 | 43, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
| 48 | | baerlem3.d |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
| 49 | 43, 48 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
| 50 | 43, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑌 ∈ (𝑉 ∖ { 0 })) |
| 51 | 43, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑍 ∈ (𝑉 ∖ { 0 })) |
| 52 | | baerlem3.a |
. . . . . . . . . . 11
⊢ ⨣ =
(+g‘𝑅) |
| 53 | | baerlem3.l |
. . . . . . . . . . 11
⊢ 𝐿 = (-g‘𝑅) |
| 54 | | baerlem3.q |
. . . . . . . . . . 11
⊢ 𝑄 = (0g‘𝑅) |
| 55 | | baerlem3.i |
. . . . . . . . . . 11
⊢ 𝐼 = (invg‘𝑅) |
| 56 | | simp12l 1287 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑎 ∈ 𝐵) |
| 57 | | simp12r 1288 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑏 ∈ 𝐵) |
| 58 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑑 ∈ 𝐵) |
| 59 | | simp2r 1201 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑒 ∈ 𝐵) |
| 60 | | simp13 1206 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) |
| 61 | | simp3 1139 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) |
| 62 | 1, 3, 42, 19, 20, 44, 45, 47, 49, 50, 51, 2, 37, 35, 36, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61 | baerlem5alem1 41710 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑗 = (𝑎 · (𝑋 − (𝑌 + 𝑍)))) |
| 63 | 43, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑊 ∈ LMod) |
| 64 | 1, 2 | lmodvacl 20873 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉) |
| 65 | 6, 11, 13, 64 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉) |
| 66 | 1, 3 | lmodvsubcl 20905 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 + 𝑍) ∈ 𝑉) → (𝑋 − (𝑌 + 𝑍)) ∈ 𝑉) |
| 67 | 6, 9, 65, 66 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 − (𝑌 + 𝑍)) ∈ 𝑉) |
| 68 | 43, 67 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → (𝑋 − (𝑌 + 𝑍)) ∈ 𝑉) |
| 69 | 1, 37, 35, 36, 20, 63, 56, 68 | ellspsni 20999 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → (𝑎 · (𝑋 − (𝑌 + 𝑍))) ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))})) |
| 70 | 62, 69 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))})) |
| 71 | 70 | 3exp 1120 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) → ((𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) → (𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌)) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))})))) |
| 72 | 71 | rexlimdvv 3212 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) → (∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌)) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))}))) |
| 73 | 72 | 3exp 1120 |
. . . . . 6
⊢ (𝜑 → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)) → (∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌)) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))}))))) |
| 74 | 73 | rexlimdvv 3212 |
. . . . 5
⊢ (𝜑 → (∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)) → (∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌)) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))})))) |
| 75 | 74 | impd 410 |
. . . 4
⊢ (𝜑 → ((∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)) ∧ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))}))) |
| 76 | 41, 75 | sylbid 240 |
. . 3
⊢ (𝜑 → (𝑗 ∈ (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) → 𝑗 ∈ (𝑁‘{(𝑋 − (𝑌 + 𝑍))}))) |
| 77 | 76 | ssrdv 3989 |
. 2
⊢ (𝜑 → (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))) ⊆ (𝑁‘{(𝑋 − (𝑌 + 𝑍))})) |
| 78 | 33, 77 | eqssd 4001 |
1
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})))) |