Proof of Theorem prjspeclsp
Step | Hyp | Ref
| Expression |
1 | | prjsprel.1 |
. . . . . . 7
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
2 | 1 | cnveqi 5717 |
. . . . . 6
⊢ ◡ ∼ = ◡{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
3 | | cnvopab 5971 |
. . . . . 6
⊢ ◡{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = {〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
4 | 2, 3 | eqtri 2761 |
. . . . 5
⊢ ◡ ∼ = {〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
5 | 4 | eceq2i 8361 |
. . . 4
⊢ [𝑋]◡ ∼ = [𝑋]{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
6 | | df-ec 8322 |
. . . . . 6
⊢ [𝑋]{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = ({〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} “ {𝑋}) |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋]{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = ({〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} “ {𝑋})) |
8 | | imaopab 39789 |
. . . . . 6
⊢
({〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} “ {𝑋}) = {𝑥 ∣ ∃𝑦 ∈ {𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → ({〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} “ {𝑋}) = {𝑥 ∣ ∃𝑦 ∈ {𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}) |
10 | | df-rex 3059 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
{𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦)) ↔ ∃𝑦(𝑦 ∈ {𝑋} ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦)))) |
11 | | velsn 4532 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑋} ↔ 𝑦 = 𝑋) |
12 | 11 | anbi1i 627 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ {𝑋} ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))) ↔ (𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦)))) |
13 | | eleq1 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑋 → (𝑦 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵)) |
14 | 13 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵))) |
15 | | oveq2 7178 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑋 → (𝑙 · 𝑦) = (𝑙 · 𝑋)) |
16 | 15 | eqeq2d 2749 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑋 → (𝑥 = (𝑙 · 𝑦) ↔ 𝑥 = (𝑙 · 𝑋))) |
17 | 16 | rexbidv 3207 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦) ↔ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))) |
18 | 14, 17 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
19 | 18 | pm5.32i 578 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))) ↔ (𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
20 | 12, 19 | bitri 278 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ {𝑋} ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))) ↔ (𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
21 | 20 | exbii 1854 |
. . . . . . . . 9
⊢
(∃𝑦(𝑦 ∈ {𝑋} ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))) ↔ ∃𝑦(𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
22 | | 19.41v 1957 |
. . . . . . . . . 10
⊢
(∃𝑦(𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))) ↔ (∃𝑦 𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
23 | | elisset 2814 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → ∃𝑦 𝑦 = 𝑋) |
24 | 23 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)) → ∃𝑦 𝑦 = 𝑋) |
25 | 24 | pm4.71ri 564 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)) ↔ (∃𝑦 𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
26 | 22, 25 | bitr4i 281 |
. . . . . . . . 9
⊢
(∃𝑦(𝑦 = 𝑋 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))) |
27 | 10, 21, 26 | 3bitri 300 |
. . . . . . . 8
⊢
(∃𝑦 ∈
{𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))) |
28 | 27 | abbii 2803 |
. . . . . . 7
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = {𝑥 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))} |
29 | | iba 531 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵))) |
30 | 29 | bicomd 226 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
31 | 30 | anbi1d 633 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
32 | 31 | abbidv 2802 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → {𝑥 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
33 | 28, 32 | syl5eq 2785 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → {𝑥 ∣ ∃𝑦 ∈ {𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
34 | 33 | adantl 485 |
. . . . 5
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → {𝑥 ∣ ∃𝑦 ∈ {𝑋} ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
35 | 7, 9, 34 | 3eqtrd 2777 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋]{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
36 | 5, 35 | syl5eq 2785 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋]◡
∼
= {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
37 | | df-rab 3062 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))} |
38 | 37 | a1i 11 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → {𝑥 ∈ 𝐵 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
39 | | prjspertr.b |
. . . . 5
⊢ 𝐵 = ((Base‘𝑉) ∖
{(0g‘𝑉)}) |
40 | 39 | rabeqi 3383 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = {𝑥 ∈ ((Base‘𝑉) ∖ {(0g‘𝑉)}) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} |
41 | | rabdif 39775 |
. . . . 5
⊢ ({𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} ∖ {(0g‘𝑉)}) = {𝑥 ∈ ((Base‘𝑉) ∖ {(0g‘𝑉)}) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} |
42 | 41 | a1i 11 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → ({𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} ∖ {(0g‘𝑉)}) = {𝑥 ∈ ((Base‘𝑉) ∖ {(0g‘𝑉)}) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)}) |
43 | 40, 42 | eqtr4id 2792 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → {𝑥 ∈ 𝐵 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = ({𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} ∖ {(0g‘𝑉)})) |
44 | 36, 38, 43 | 3eqtr2d 2779 |
. 2
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋]◡
∼
= ({𝑥 ∈
(Base‘𝑉) ∣
∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} ∖ {(0g‘𝑉)})) |
45 | | prjspertr.s |
. . . . . 6
⊢ 𝑆 = (Scalar‘𝑉) |
46 | | prjspertr.x |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑉) |
47 | | prjspertr.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝑆) |
48 | 1, 39, 45, 46, 47 | prjsper 40024 |
. . . . 5
⊢ (𝑉 ∈ LVec → ∼ Er
𝐵) |
49 | 48 | adantr 484 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → ∼ Er 𝐵) |
50 | | ercnv 8341 |
. . . . 5
⊢ ( ∼ Er
𝐵 → ◡ ∼ = ∼
) |
51 | 50 | eqcomd 2744 |
. . . 4
⊢ ( ∼ Er
𝐵 → ∼ = ◡ ∼ ) |
52 | 49, 51 | syl 17 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → ∼ = ◡ ∼ ) |
53 | 52 | eceq2d 8362 |
. 2
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋] ∼ = [𝑋]◡ ∼ ) |
54 | | lveclmod 19997 |
. . . . 5
⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod) |
55 | | difss 4022 |
. . . . . . 7
⊢
((Base‘𝑉)
∖ {(0g‘𝑉)}) ⊆ (Base‘𝑉) |
56 | 39, 55 | eqsstri 3911 |
. . . . . 6
⊢ 𝐵 ⊆ (Base‘𝑉) |
57 | 56 | sseli 3873 |
. . . . 5
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘𝑉)) |
58 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑉) =
(Base‘𝑉) |
59 | | prjsprellsp.n |
. . . . . 6
⊢ 𝑁 = (LSpan‘𝑉) |
60 | 45, 47, 58, 46, 59 | lspsn 19893 |
. . . . 5
⊢ ((𝑉 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑉)) → (𝑁‘{𝑋}) = {𝑥 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)}) |
61 | 54, 57, 60 | syl2an 599 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → (𝑁‘{𝑋}) = {𝑥 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)}) |
62 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) ∧ 𝑥 = (𝑙 · 𝑋)) → 𝑥 = (𝑙 · 𝑋)) |
63 | 54 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → 𝑉 ∈ LMod) |
64 | 63 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) → 𝑉 ∈ LMod) |
65 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) → 𝑙 ∈ 𝐾) |
66 | 57 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) → 𝑋 ∈ (Base‘𝑉)) |
67 | 58, 45, 46, 47 | lmodvscl 19770 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ 𝑋 ∈ (Base‘𝑉)) → (𝑙 · 𝑋) ∈ (Base‘𝑉)) |
68 | 64, 65, 66, 67 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) → (𝑙 · 𝑋) ∈ (Base‘𝑉)) |
69 | 68 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) ∧ 𝑥 = (𝑙 · 𝑋)) → (𝑙 · 𝑋) ∈ (Base‘𝑉)) |
70 | 62, 69 | eqeltrd 2833 |
. . . . . . . 8
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) ∧ 𝑙 ∈ 𝐾) ∧ 𝑥 = (𝑙 · 𝑋)) → 𝑥 ∈ (Base‘𝑉)) |
71 | 70 | rexlimdva2 3197 |
. . . . . . 7
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → (∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋) → 𝑥 ∈ (Base‘𝑉))) |
72 | 71 | pm4.71rd 566 |
. . . . . 6
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → (∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋) ↔ (𝑥 ∈ (Base‘𝑉) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)))) |
73 | 72 | abbidv 2802 |
. . . . 5
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → {𝑥 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = {𝑥 ∣ (𝑥 ∈ (Base‘𝑉) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))}) |
74 | | df-rab 3062 |
. . . . 5
⊢ {𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = {𝑥 ∣ (𝑥 ∈ (Base‘𝑉) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋))} |
75 | 73, 74 | eqtr4di 2791 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → {𝑥 ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} = {𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)}) |
76 | 61, 75 | eqtrd 2773 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → (𝑁‘{𝑋}) = {𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)}) |
77 | 76 | difeq1d 4012 |
. 2
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → ((𝑁‘{𝑋}) ∖ {(0g‘𝑉)}) = ({𝑥 ∈ (Base‘𝑉) ∣ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑋)} ∖ {(0g‘𝑉)})) |
78 | 44, 53, 77 | 3eqtr4d 2783 |
1
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋] ∼ = ((𝑁‘{𝑋}) ∖ {(0g‘𝑉)})) |