Step | Hyp | Ref
| Expression |
1 | | lspsneq.w |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lveclmod 19594 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | | lspsneq.s |
. . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑊) |
5 | 4 | lmodring 19358 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑆 ∈ Ring) |
6 | | lspsneq.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑆) |
7 | | eqid 2775 |
. . . . . . . . . 10
⊢
(1r‘𝑆) = (1r‘𝑆) |
8 | 6, 7 | ringidcl 19035 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝐾) |
9 | 3, 5, 8 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑆) ∈ 𝐾) |
10 | 4 | lvecdrng 19593 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑆 ∈
DivRing) |
11 | | lspsneq.o |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑆) |
12 | 11, 7 | drngunz 19234 |
. . . . . . . . 9
⊢ (𝑆 ∈ DivRing →
(1r‘𝑆)
≠ 0
) |
13 | 1, 10, 12 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑆) ≠ 0 ) |
14 | | eldifsn 4591 |
. . . . . . . 8
⊢
((1r‘𝑆) ∈ (𝐾 ∖ { 0 }) ↔
((1r‘𝑆)
∈ 𝐾 ∧
(1r‘𝑆)
≠ 0
)) |
15 | 9, 13, 14 | sylanbrc 575 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑆) ∈ (𝐾 ∖ { 0 })) |
16 | 15 | ad2antrr 713 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → (1r‘𝑆) ∈ (𝐾 ∖ { 0 })) |
17 | | lspsneq.v |
. . . . . . . . . . 11
⊢ 𝑉 = (Base‘𝑊) |
18 | | eqid 2775 |
. . . . . . . . . . 11
⊢
(0g‘𝑊) = (0g‘𝑊) |
19 | 17, 18 | lmod0vcl 19379 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ 𝑉) |
20 | 1, 2, 19 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑊) ∈ 𝑉) |
21 | | lspsneq.t |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
22 | 17, 4, 21, 7 | lmodvs1 19378 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧
(0g‘𝑊)
∈ 𝑉) →
((1r‘𝑆)
·
(0g‘𝑊)) =
(0g‘𝑊)) |
23 | 3, 20, 22 | syl2anc 576 |
. . . . . . . 8
⊢ (𝜑 →
((1r‘𝑆)
·
(0g‘𝑊)) =
(0g‘𝑊)) |
24 | 23 | ad2antrr 713 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → ((1r‘𝑆) ·
(0g‘𝑊)) =
(0g‘𝑊)) |
25 | | oveq2 6982 |
. . . . . . . 8
⊢ (𝑌 = (0g‘𝑊) →
((1r‘𝑆)
·
𝑌) =
((1r‘𝑆)
·
(0g‘𝑊))) |
26 | 25 | adantl 474 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → ((1r‘𝑆) · 𝑌) = ((1r‘𝑆) ·
(0g‘𝑊))) |
27 | | lspsneq.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑊) |
28 | 3 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑊 ∈ LMod) |
29 | | lspsneq.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
30 | 29 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑋 ∈ 𝑉) |
31 | | lspsneq.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
32 | 31 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑌 ∈ 𝑉) |
33 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) |
34 | 17, 18, 27, 28, 30, 32, 33 | lspsneq0b 19501 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 = (0g‘𝑊) ↔ 𝑌 = (0g‘𝑊))) |
35 | 34 | biimpar 470 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → 𝑋 = (0g‘𝑊)) |
36 | 24, 26, 35 | 3eqtr4rd 2822 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → 𝑋 = ((1r‘𝑆) · 𝑌)) |
37 | | oveq1 6981 |
. . . . . . 7
⊢ (𝑗 = (1r‘𝑆) → (𝑗 · 𝑌) = ((1r‘𝑆) · 𝑌)) |
38 | 37 | rspceeqv 3550 |
. . . . . 6
⊢
(((1r‘𝑆) ∈ (𝐾 ∖ { 0 }) ∧ 𝑋 = ((1r‘𝑆) · 𝑌)) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
39 | 16, 36, 38 | syl2anc 576 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 = (0g‘𝑊)) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
40 | | eqimss 3912 |
. . . . . . . . . 10
⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) |
41 | 40 | adantl 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) |
42 | | eqid 2775 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
43 | 17, 42, 27 | lspsncl 19465 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
44 | 3, 31, 43 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
45 | 44 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
46 | 17, 42, 27, 28, 45, 30 | lspsnel5 19483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 ∈ (𝑁‘{𝑌}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}))) |
47 | 41, 46 | mpbird 249 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑋 ∈ (𝑁‘{𝑌})) |
48 | 4, 6, 17, 21, 27 | lspsnel 19491 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑋 ∈ (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌))) |
49 | 28, 32, 48 | syl2anc 576 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 ∈ (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌))) |
50 | 47, 49 | mpbid 224 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌)) |
51 | 50 | adantr 473 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → ∃𝑗 ∈ 𝐾 𝑋 = (𝑗 · 𝑌)) |
52 | | simprl 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑗 ∈ 𝐾) |
53 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌)) → 𝑋 = (𝑗 · 𝑌)) |
54 | 53 | adantl 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑋 = (𝑗 · 𝑌)) |
55 | 34 | biimpd 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑋 = (0g‘𝑊) → 𝑌 = (0g‘𝑊))) |
56 | 55 | necon3d 2985 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → (𝑌 ≠ (0g‘𝑊) → 𝑋 ≠ (0g‘𝑊))) |
57 | 56 | imp 398 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑋 ≠ (0g‘𝑊)) |
58 | 57 | adantr 473 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑋 ≠ (0g‘𝑊)) |
59 | 54, 58 | eqnetrrd 3032 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → (𝑗 · 𝑌) ≠ (0g‘𝑊)) |
60 | 1 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → 𝑊 ∈ LVec) |
61 | 60 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑊 ∈ LVec) |
62 | 32 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑌 ∈ 𝑉) |
63 | 17, 21, 4, 6, 11, 18, 61, 52, 62 | lvecvsn0 19597 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → ((𝑗 · 𝑌) ≠ (0g‘𝑊) ↔ (𝑗 ≠ 0 ∧ 𝑌 ≠ (0g‘𝑊)))) |
64 | 59, 63 | mpbid 224 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → (𝑗 ≠ 0 ∧ 𝑌 ≠ (0g‘𝑊))) |
65 | 64 | simpld 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑗 ≠ 0 ) |
66 | | eldifsn 4591 |
. . . . . . 7
⊢ (𝑗 ∈ (𝐾 ∖ { 0 }) ↔ (𝑗 ∈ 𝐾 ∧ 𝑗 ≠ 0 )) |
67 | 52, 65, 66 | sylanbrc 575 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑗 ∈ 𝐾 ∧ 𝑋 = (𝑗 · 𝑌))) → 𝑗 ∈ (𝐾 ∖ { 0 })) |
68 | 51, 67, 54 | reximssdv 3218 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ 𝑌 ≠ (0g‘𝑊)) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
69 | 39, 68 | pm2.61dane 3052 |
. . . 4
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌)) |
70 | 69 | ex 405 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌))) |
71 | 1 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑊 ∈ LVec) |
72 | | eldifi 3992 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝐾 ∖ { 0 }) → 𝑗 ∈ 𝐾) |
73 | 72 | adantl 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑗 ∈ 𝐾) |
74 | | eldifsni 4594 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝐾 ∖ { 0 }) → 𝑗 ≠ 0 ) |
75 | 74 | adantl 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑗 ≠ 0 ) |
76 | 31 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → 𝑌 ∈ 𝑉) |
77 | 17, 4, 21, 6, 11, 27 | lspsnvs 19602 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ (𝑗 ∈ 𝐾 ∧ 𝑗 ≠ 0 ) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌})) |
78 | 71, 73, 75, 76, 77 | syl121anc 1355 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐾 ∖ { 0 })) → (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌})) |
79 | 78 | ex 405 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ (𝐾 ∖ { 0 }) → (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌}))) |
80 | | sneq 4449 |
. . . . . . 7
⊢ (𝑋 = (𝑗 · 𝑌) → {𝑋} = {(𝑗 · 𝑌)}) |
81 | 80 | fveqeq2d 6505 |
. . . . . 6
⊢ (𝑋 = (𝑗 · 𝑌) → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ (𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌}))) |
82 | 81 | biimprcd 242 |
. . . . 5
⊢ ((𝑁‘{(𝑗 · 𝑌)}) = (𝑁‘{𝑌}) → (𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
83 | 79, 82 | syl6 35 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ (𝐾 ∖ { 0 }) → (𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌})))) |
84 | 83 | rexlimdv 3225 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
85 | 70, 84 | impbid 204 |
. 2
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌))) |
86 | | oveq1 6981 |
. . . 4
⊢ (𝑗 = 𝑘 → (𝑗 · 𝑌) = (𝑘 · 𝑌)) |
87 | 86 | eqeq2d 2785 |
. . 3
⊢ (𝑗 = 𝑘 → (𝑋 = (𝑗 · 𝑌) ↔ 𝑋 = (𝑘 · 𝑌))) |
88 | 87 | cbvrexv 3381 |
. 2
⊢
(∃𝑗 ∈
(𝐾 ∖ { 0 })𝑋 = (𝑗 · 𝑌) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌)) |
89 | 85, 88 | syl6bb 279 |
1
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌))) |