| Step | Hyp | Ref
| Expression |
| 1 | | simpllr 776 |
. . . 4
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑋 ∼ 𝑌) |
| 2 | | prjsprel.1 |
. . . . . 6
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
| 3 | 2 | prjsprel 42614 |
. . . . 5
⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) |
| 4 | | pm3.22 459 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
| 5 | 4 | adantr 480 |
. . . . 5
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) → (𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
| 6 | 3, 5 | sylbi 217 |
. . . 4
⊢ (𝑋 ∼ 𝑌 → (𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
| 7 | 1, 6 | syl 17 |
. . 3
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → (𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
| 8 | | oveq1 7438 |
. . . . 5
⊢ (𝑛 = ((invr‘𝑆)‘𝑚) → (𝑛 · 𝑋) = (((invr‘𝑆)‘𝑚) · 𝑋)) |
| 9 | 8 | eqeq2d 2748 |
. . . 4
⊢ (𝑛 = ((invr‘𝑆)‘𝑚) → (𝑌 = (𝑛 · 𝑋) ↔ 𝑌 = (((invr‘𝑆)‘𝑚) · 𝑋))) |
| 10 | | simplll 775 |
. . . . . 6
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑉 ∈ LVec) |
| 11 | | prjspertr.s |
. . . . . . 7
⊢ 𝑆 = (Scalar‘𝑉) |
| 12 | 11 | lvecdrng 21104 |
. . . . . 6
⊢ (𝑉 ∈ LVec → 𝑆 ∈
DivRing) |
| 13 | 10, 12 | syl 17 |
. . . . 5
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑆 ∈ DivRing) |
| 14 | | simplr 769 |
. . . . 5
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑚 ∈ 𝐾) |
| 15 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) → 𝑋 ∈ 𝐵) |
| 16 | 3, 15 | sylbi 217 |
. . . . . . 7
⊢ (𝑋 ∼ 𝑌 → 𝑋 ∈ 𝐵) |
| 17 | | eldifsni 4790 |
. . . . . . . 8
⊢ (𝑋 ∈ ((Base‘𝑉) ∖
{(0g‘𝑉)})
→ 𝑋 ≠
(0g‘𝑉)) |
| 18 | | prjspertr.b |
. . . . . . . 8
⊢ 𝐵 = ((Base‘𝑉) ∖
{(0g‘𝑉)}) |
| 19 | 17, 18 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ≠ (0g‘𝑉)) |
| 20 | 1, 16, 19 | 3syl 18 |
. . . . . 6
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑋 ≠ (0g‘𝑉)) |
| 21 | | simplr 769 |
. . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → 𝑋 = (𝑚 · 𝑌)) |
| 22 | | simpr 484 |
. . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → 𝑚 = (0g‘𝑆)) |
| 23 | 22 | oveq1d 7446 |
. . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → (𝑚 · 𝑌) = ((0g‘𝑆) · 𝑌)) |
| 24 | | lveclmod 21105 |
. . . . . . . . 9
⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod) |
| 25 | 24 | ad4antr 732 |
. . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → 𝑉 ∈ LMod) |
| 26 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) → 𝑌 ∈ 𝐵) |
| 27 | 3, 26 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑋 ∼ 𝑌 → 𝑌 ∈ 𝐵) |
| 28 | | eldifi 4131 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ((Base‘𝑉) ∖
{(0g‘𝑉)})
→ 𝑌 ∈
(Base‘𝑉)) |
| 29 | 28, 18 | eleq2s 2859 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ (Base‘𝑉)) |
| 30 | 1, 27, 29 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑌 ∈ (Base‘𝑉)) |
| 31 | 30 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → 𝑌 ∈ (Base‘𝑉)) |
| 32 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑉) =
(Base‘𝑉) |
| 33 | | prjspertr.x |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑉) |
| 34 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑆) = (0g‘𝑆) |
| 35 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑉) = (0g‘𝑉) |
| 36 | 32, 11, 33, 34, 35 | lmod0vs 20893 |
. . . . . . . 8
⊢ ((𝑉 ∈ LMod ∧ 𝑌 ∈ (Base‘𝑉)) →
((0g‘𝑆)
·
𝑌) =
(0g‘𝑉)) |
| 37 | 25, 31, 36 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → ((0g‘𝑆) · 𝑌) = (0g‘𝑉)) |
| 38 | 21, 23, 37 | 3eqtrd 2781 |
. . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = (0g‘𝑆)) → 𝑋 = (0g‘𝑉)) |
| 39 | 20, 38 | mteqand 3033 |
. . . . 5
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑚 ≠ (0g‘𝑆)) |
| 40 | | prjspertr.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝑆) |
| 41 | | eqid 2737 |
. . . . . 6
⊢
(invr‘𝑆) = (invr‘𝑆) |
| 42 | 40, 34, 41 | drnginvrcl 20753 |
. . . . 5
⊢ ((𝑆 ∈ DivRing ∧ 𝑚 ∈ 𝐾 ∧ 𝑚 ≠ (0g‘𝑆)) → ((invr‘𝑆)‘𝑚) ∈ 𝐾) |
| 43 | 13, 14, 39, 42 | syl3anc 1373 |
. . . 4
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → ((invr‘𝑆)‘𝑚) ∈ 𝐾) |
| 44 | | simpr 484 |
. . . . 5
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑋 = (𝑚 · 𝑌)) |
| 45 | | nelsn 4666 |
. . . . . . . 8
⊢ (𝑚 ≠ (0g‘𝑆) → ¬ 𝑚 ∈
{(0g‘𝑆)}) |
| 46 | 39, 45 | syl 17 |
. . . . . . 7
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → ¬ 𝑚 ∈ {(0g‘𝑆)}) |
| 47 | 14, 46 | eldifd 3962 |
. . . . . 6
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑚 ∈ (𝐾 ∖ {(0g‘𝑆)})) |
| 48 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑋 ∈ ((Base‘𝑉) ∖
{(0g‘𝑉)})
→ 𝑋 ∈
(Base‘𝑉)) |
| 49 | 48, 18 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘𝑉)) |
| 50 | 1, 16, 49 | 3syl 18 |
. . . . . 6
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑋 ∈ (Base‘𝑉)) |
| 51 | 32, 33, 11, 40, 34, 41, 10, 47, 50, 30 | lvecinv 21115 |
. . . . 5
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → (𝑋 = (𝑚 · 𝑌) ↔ 𝑌 = (((invr‘𝑆)‘𝑚) · 𝑋))) |
| 52 | 44, 51 | mpbid 232 |
. . . 4
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑌 = (((invr‘𝑆)‘𝑚) · 𝑋)) |
| 53 | 9, 43, 52 | rspcedvdw 3625 |
. . 3
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → ∃𝑛 ∈ 𝐾 𝑌 = (𝑛 · 𝑋)) |
| 54 | 2 | prjsprel 42614 |
. . 3
⊢ (𝑌 ∼ 𝑋 ↔ ((𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ∃𝑛 ∈ 𝐾 𝑌 = (𝑛 · 𝑋))) |
| 55 | 7, 53, 54 | sylanbrc 583 |
. 2
⊢ ((((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) ∧ 𝑚 ∈ 𝐾) ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑌 ∼ 𝑋) |
| 56 | | simpr 484 |
. . . 4
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) → ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) |
| 57 | 3, 56 | sylbi 217 |
. . 3
⊢ (𝑋 ∼ 𝑌 → ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) |
| 58 | 57 | adantl 481 |
. 2
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) |
| 59 | 55, 58 | r19.29a 3162 |
1
⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋) |