Step | Hyp | Ref
| Expression |
1 | | lspsneq.w |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lveclmod 18927 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | | lspsneq.s |
. . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑊) |
5 | 4 | lmodring 18694 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑆 ∈ Ring) |
6 | | lspsneq.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑆) |
7 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1r‘𝑆) = (1r‘𝑆) |
8 | 6, 7 | ringidcl 18391 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝐾) |
9 | 3, 5, 8 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑆) ∈ 𝐾) |
10 | 4 | lvecdrng 18926 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑆 ∈
DivRing) |
11 | | lspsneq.o |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑆) |
12 | 11, 7 | drngunz 18585 |
. . . . . . . . 9
⊢ (𝑆 ∈ DivRing →
(1r‘𝑆)
≠ 0
) |
13 | 1, 10, 12 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑆) ≠ 0 ) |
14 | | eldifsn 4260 |
. . . . . . . 8
⊢
((1r‘𝑆) ∈ (𝐾 ∖ { 0 }) ↔
((1r‘𝑆)
∈ 𝐾 ∧
(1r‘𝑆)
≠ 0
)) |
15 | 9, 13, 14 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑆) ∈ (𝐾 ∖ { 0 })) |
16 | 15 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → (1r‘𝑆) ∈ (𝐾 ∖ { 0 })) |
17 | | lspsneq.v |
. . . . . . . . . . 11
⊢ 𝑉 = (Base‘𝑊) |
18 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑊) = (0g‘𝑊) |
19 | 17, 18 | lmod0vcl 18715 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ 𝑉) |
20 | 1, 2, 19 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑊) ∈ 𝑉) |
21 | | lspsneq.t |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
22 | 17, 4, 21, 7 | lmodvs1 18714 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧
(0g‘𝑊)
∈ 𝑉) →
((1r‘𝑆)
·
(0g‘𝑊)) =
(0g‘𝑊)) |
23 | 3, 20, 22 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 →
((1r‘𝑆)
·
(0g‘𝑊)) =
(0g‘𝑊)) |
24 | 23 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → ((1r‘𝑆) ·
(0g‘𝑊)) =
(0g‘𝑊)) |
25 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑌 = (0g‘𝑊) →
((1r‘𝑆)
·
𝑌) =
((1r‘𝑆)
·
(0g‘𝑊))) |
26 | 25 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → ((1r‘𝑆) · 𝑌) = ((1r‘𝑆) ·
(0g‘𝑊))) |
27 | | lspsneq.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑊) |
28 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑊 ∈ LMod) |
29 | | lspsneq.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
30 | 29 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑋 ∈ 𝑉) |
31 | | lspsneq.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑌 ∈ 𝑉) |
33 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) |
34 | 17, 18, 27, 28, 30, 32, 33 | lspsneq0b 18834 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 = (0g‘𝑊) ↔ 𝑌 = (0g‘𝑊))) |
35 | 34 | biimpar 501 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → 𝑋 = (0g‘𝑊)) |
36 | 24, 26, 35 | 3eqtr4rd 2655 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → 𝑋 = ((1r‘𝑆) · 𝑌)) |
37 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑗 = (1r‘𝑆) → (𝑗 · 𝑌) = ((1r‘𝑆) · 𝑌)) |
38 | 37 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑗 = (1r‘𝑆) → (𝑋 = (𝑗 · 𝑌) ↔ 𝑋 = ((1r‘𝑆) · 𝑌))) |
39 | 38 | rspcev 3282 |
. . . . . 6
⊢
(((1r‘𝑆) ∈ (𝐾 ∖ { 0 }) ∧ 𝑋 = ((1r‘𝑆) · 𝑌)) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
40 | 16, 36, 39 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
41 | | eqimss 3620 |
. . . . . . . . . 10
⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) |
42 | 41 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) |
43 | | eqid 2610 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
44 | 17, 43, 27 | lspsncl 18798 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
45 | 3, 31, 44 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
46 | 45 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
47 | 17, 43, 27, 28, 46, 30 | lspsnel5 18816 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 ∈ (𝑁‘{𝑌}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}))) |
48 | 42, 47 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑋 ∈ (𝑁‘{𝑌})) |
49 | 4, 6, 17, 21, 27 | lspsnel 18824 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑋 ∈ (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌))) |
50 | 28, 32, 49 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 ∈ (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌))) |
51 | 48, 50 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌)) |
52 | 51 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌)) |
53 | | simprl 790 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑗 ∈ 𝐾) |
54 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌)) → 𝑋 = (𝑗 · 𝑌)) |
55 | 54 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑋 = (𝑗 · 𝑌)) |
56 | 34 | biimpd 218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 = (0g‘𝑊) → 𝑌 = (0g‘𝑊))) |
57 | 56 | necon3d 2803 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑌 ≠ (0g‘𝑊) → 𝑋 ≠ (0g‘𝑊))) |
58 | 57 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑋 ≠ (0g‘𝑊)) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑋 ≠ (0g‘𝑊)) |
60 | 55, 59 | eqnetrrd 2850 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → (𝑗 · 𝑌) ≠ (0g‘𝑊)) |
61 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑊 ∈ LVec) |
62 | 61 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑊 ∈ LVec) |
63 | 32 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑌 ∈ 𝑉) |
64 | 17, 21, 4, 6, 11, 18, 62, 53, 63 | lvecvsn0 18930 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → ((𝑗 · 𝑌) ≠ (0g‘𝑊) ↔ (𝑗 ≠ 0 ∧ 𝑌 ≠ (0g‘𝑊)))) |
65 | 60, 64 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → (𝑗 ≠ 0 ∧ 𝑌 ≠ (0g‘𝑊))) |
66 | 65 | simpld 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑗 ≠ 0 ) |
67 | | eldifsn 4260 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐾 ∖ { 0 }) ↔ (𝑗 ∈ 𝐾 ∧ 𝑗 ≠ 0 )) |
68 | 53, 66, 67 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑗 ∈ (𝐾 ∖ { 0 })) |
69 | 68, 55 | jca 553 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → (𝑗 ∈ (𝐾 ∖ { 0 }) ∧ 𝑋 = (𝑗 · 𝑌))) |
70 | 69 | ex 449 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌)) → (𝑗 ∈ (𝐾 ∖ { 0 }) ∧ 𝑋 = (𝑗 · 𝑌)))) |
71 | 70 | reximdv2 2997 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → (∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌))) |
72 | 52, 71 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
73 | 40, 72 | pm2.61dane 2869 |
. . . 4
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
74 | 73 | ex 449 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌))) |
75 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑊 ∈ LVec) |
76 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝐾 ∖ { 0 }) → 𝑗 ∈ 𝐾) |
77 | 76 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑗 ∈ 𝐾) |
78 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝐾 ∖ { 0 }) → 𝑗 ≠ 0 ) |
79 | 78 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑗 ≠ 0 ) |
80 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑌 ∈ 𝑉) |
81 | 17, 4, 21, 6, 11, 27 | lspsnvs 18935 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ (𝑗 ∈ 𝐾 ∧ 𝑗 ≠ 0 ) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌})) |
82 | 75, 77, 79, 80, 81 | syl121anc 1323 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌})) |
83 | 82 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ (𝐾 ∖ { 0 }) → (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌}))) |
84 | | sneq 4135 |
. . . . . . . 8
⊢ (𝑋 = (𝑗 · 𝑌) → {𝑋} = {(𝑗 · 𝑌)}) |
85 | 84 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{(𝑗 · 𝑌)})) |
86 | 85 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑋 = (𝑗 · 𝑌) → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌}))) |
87 | 86 | biimprcd 239 |
. . . . 5
⊢ ((𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌}) → (𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
88 | 83, 87 | syl6 34 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ (𝐾 ∖ { 0 }) → (𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌})))) |
89 | 88 | rexlimdv 3012 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
90 | 74, 89 | impbid 201 |
. 2
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌))) |
91 | | oveq1 6556 |
. . . 4
⊢ (𝑗 = 𝑘 → (𝑗 · 𝑌) = (𝑘 · 𝑌)) |
92 | 91 | eqeq2d 2620 |
. . 3
⊢ (𝑗 = 𝑘 → (𝑋 = (𝑗 · 𝑌) ↔ 𝑋 = (𝑘 · 𝑌))) |
93 | 92 | cbvrexv 3148 |
. 2
⊢
(∃𝑗 ∈
(𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌)) |
94 | 90, 93 | syl6bb 275 |
1
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌))) |