Proof of Theorem prjspreln0
Step | Hyp | Ref
| Expression |
1 | | prjsprel.1 |
. . 3
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} |
2 | 1 | prjsprel 40199 |
. 2
⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) |
3 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) → 𝑚 ∈ 𝐾) |
4 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) → 𝑋 ∈ 𝐵) |
5 | | eldifsni 4720 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ((Base‘𝑉) ∖
{(0g‘𝑉)})
→ 𝑋 ≠
(0g‘𝑉)) |
6 | | prjspertr.b |
. . . . . . . . . . . 12
⊢ 𝐵 = ((Base‘𝑉) ∖
{(0g‘𝑉)}) |
7 | 5, 6 | eleq2s 2858 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐵 → 𝑋 ≠ (0g‘𝑉)) |
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) → 𝑋 ≠ (0g‘𝑉)) |
9 | | simplrr 778 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → 𝑋 = (𝑚 · 𝑌)) |
10 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → 𝑚 = 0 ) |
11 | 10 | oveq1d 7250 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → (𝑚 · 𝑌) = ( 0 · 𝑌)) |
12 | | lveclmod 20176 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod) |
13 | 12 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → 𝑉 ∈ LMod) |
14 | | difss 4063 |
. . . . . . . . . . . . . 14
⊢
((Base‘𝑉)
∖ {(0g‘𝑉)}) ⊆ (Base‘𝑉) |
15 | 6, 14 | eqsstri 3952 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ (Base‘𝑉) |
16 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ ((𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌)) ∧ 𝑚 = 0 )) → 𝑌 ∈ 𝐵) |
17 | 16 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → 𝑌 ∈ 𝐵) |
18 | 15, 17 | sseldi 3916 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → 𝑌 ∈ (Base‘𝑉)) |
19 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑉) =
(Base‘𝑉) |
20 | | prjspertr.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (Scalar‘𝑉) |
21 | | prjspertr.x |
. . . . . . . . . . . . 13
⊢ · = (
·𝑠 ‘𝑉) |
22 | | prjspreln0.z |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝑆) |
23 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑉) = (0g‘𝑉) |
24 | 19, 20, 21, 22, 23 | lmod0vs 19965 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ LMod ∧ 𝑌 ∈ (Base‘𝑉)) → ( 0 · 𝑌) = (0g‘𝑉)) |
25 | 13, 18, 24 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → ( 0 · 𝑌) = (0g‘𝑉)) |
26 | 9, 11, 25 | 3eqtrd 2783 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) ∧ 𝑚 = 0 ) → 𝑋 = (0g‘𝑉)) |
27 | 8, 26 | mteqand 3048 |
. . . . . . . . 9
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) → 𝑚 ≠ 0 ) |
28 | | nelsn 4598 |
. . . . . . . . 9
⊢ (𝑚 ≠ 0 → ¬ 𝑚 ∈ { 0 }) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) → ¬ 𝑚 ∈ { 0 }) |
30 | 3, 29 | eldifd 3894 |
. . . . . . 7
⊢ (((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌))) → 𝑚 ∈ (𝐾 ∖ { 0 })) |
31 | 30 | ex 416 |
. . . . . 6
⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑚 ∈ (𝐾 ∖ { 0 }))) |
32 | | simpr 488 |
. . . . . 6
⊢ ((𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌)) → 𝑋 = (𝑚 · 𝑌)) |
33 | 31, 32 | jca2 517 |
. . . . 5
⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑚 ∈ 𝐾 ∧ 𝑋 = (𝑚 · 𝑌)) → (𝑚 ∈ (𝐾 ∖ { 0 }) ∧ 𝑋 = (𝑚 · 𝑌)))) |
34 | 33 | reximdv2 3199 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌) → ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌))) |
35 | | difss 4063 |
. . . . 5
⊢ (𝐾 ∖ { 0 }) ⊆ 𝐾 |
36 | | ssrexv 3985 |
. . . . 5
⊢ ((𝐾 ∖ { 0 }) ⊆ 𝐾 → (∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌) → ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) |
37 | 35, 36 | mp1i 13 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌) → ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) |
38 | 34, 37 | impbid 215 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌) ↔ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌))) |
39 | 38 | pm5.32da 582 |
. 2
⊢ (𝑉 ∈ LVec → (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)) ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌)))) |
40 | 2, 39 | syl5bb 286 |
1
⊢ (𝑉 ∈ LVec → (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌)))) |