Step | Hyp | Ref
| Expression |
1 | | 0nn0 11766 |
. . 3
⊢ 0 ∈
ℕ0 |
2 | | eqid 2797 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} |
3 | | 0prjspn.w |
. . . 4
⊢ 𝑊 = (𝐾 freeLMod (0...0)) |
4 | | 0prjspn.b |
. . . 4
⊢ 𝐵 = ((Base‘𝑊) ∖
{(0g‘𝑊)}) |
5 | | eqid 2797 |
. . . 4
⊢
(Base‘𝐾) =
(Base‘𝐾) |
6 | | eqid 2797 |
. . . 4
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
7 | 2, 3, 4, 5, 6 | prjspnval2 38785 |
. . 3
⊢ ((0
∈ ℕ0 ∧ 𝐾 ∈ DivRing) →
(0ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))})) |
8 | 1, 7 | mpan 686 |
. 2
⊢ (𝐾 ∈ DivRing →
(0ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))})) |
9 | | ovex 7055 |
. . . . . . . 8
⊢ (0...0)
∈ V |
10 | 3 | frlmsca 20583 |
. . . . . . . 8
⊢ ((𝐾 ∈ DivRing ∧ (0...0)
∈ V) → 𝐾 =
(Scalar‘𝑊)) |
11 | 9, 10 | mpan2 687 |
. . . . . . 7
⊢ (𝐾 ∈ DivRing → 𝐾 = (Scalar‘𝑊)) |
12 | 11 | fveq2d 6549 |
. . . . . 6
⊢ (𝐾 ∈ DivRing →
(Base‘𝐾) =
(Base‘(Scalar‘𝑊))) |
13 | 12 | rexeqdv 3378 |
. . . . 5
⊢ (𝐾 ∈ DivRing →
(∃𝑙 ∈
(Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦) ↔ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))) |
14 | 13 | anbi2d 628 |
. . . 4
⊢ (𝐾 ∈ DivRing → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦)))) |
15 | 14 | opabbidv 5034 |
. . 3
⊢ (𝐾 ∈ DivRing →
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}) |
16 | 15 | qseq2d 8203 |
. 2
⊢ (𝐾 ∈ DivRing → (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}) = (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))})) |
17 | 3 | frlmlvec 20591 |
. . . . . . 7
⊢ ((𝐾 ∈ DivRing ∧ (0...0)
∈ V) → 𝑊 ∈
LVec) |
18 | 9, 17 | mpan2 687 |
. . . . . 6
⊢ (𝐾 ∈ DivRing → 𝑊 ∈ LVec) |
19 | | lveclmod 19572 |
. . . . . 6
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ DivRing → 𝑊 ∈ LMod) |
21 | 20 | adantr 481 |
. . . 4
⊢ ((𝐾 ∈ DivRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑊 ∈ LMod) |
22 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}) |
23 | | eqid 2797 |
. . . . . . 7
⊢ ((𝐾 unitVec (0...0))‘0) =
((𝐾 unitVec
(0...0))‘0) |
24 | 2, 4, 6, 5, 3, 23 | 0prjspnrel 38787 |
. . . . . 6
⊢ ((𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵) → 𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) |
25 | 22, 24 | breqdi 4983 |
. . . . 5
⊢ ((𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵) → 𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) |
26 | 25 | adantrr 713 |
. . . 4
⊢ ((𝐾 ∈ DivRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) |
27 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}) |
28 | 2, 4, 6, 5, 3, 23 | 0prjspnrel 38787 |
. . . . . . 7
⊢ ((𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵) → 𝑏{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) |
29 | 27, 28 | breqdi 4983 |
. . . . . 6
⊢ ((𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵) → 𝑏{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) |
30 | | eqid 2797 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} |
31 | | eqid 2797 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
32 | | eqid 2797 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
33 | 30, 4, 31, 6, 32 | prjspersym 38775 |
. . . . . 6
⊢ ((𝑊 ∈ LVec ∧ 𝑏{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) → ((𝐾 unitVec
(0...0))‘0){〈𝑥,
𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}𝑏) |
34 | 18, 29, 33 | syl2an2r 681 |
. . . . 5
⊢ ((𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵) → ((𝐾 unitVec (0...0))‘0){〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}𝑏) |
35 | 34 | adantrl 712 |
. . . 4
⊢ ((𝐾 ∈ DivRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐾 unitVec (0...0))‘0){〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}𝑏) |
36 | 30, 4, 31, 6, 32 | prjspertr 38773 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0) ∧ ((𝐾 unitVec
(0...0))‘0){〈𝑥,
𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}𝑏)) → 𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}𝑏) |
37 | 21, 26, 35, 36 | syl12anc 833 |
. . 3
⊢ ((𝐾 ∈ DivRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}𝑏) |
38 | 30, 4, 31, 6, 32 | prjsper 38776 |
. . . 4
⊢ (𝑊 ∈ LVec → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} Er 𝐵) |
39 | 18, 38 | syl 17 |
. . 3
⊢ (𝐾 ∈ DivRing →
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))} Er 𝐵) |
40 | 4, 3, 23 | 0prjspnlem 38786 |
. . 3
⊢ (𝐾 ∈ DivRing → ((𝐾 unitVec (0...0))‘0)
∈ 𝐵) |
41 | | fvex 6558 |
. . . . . 6
⊢
(Base‘𝑊)
∈ V |
42 | 41 | difexi 5130 |
. . . . 5
⊢
((Base‘𝑊)
∖ {(0g‘𝑊)}) ∈ V |
43 | 4, 42 | eqeltri 2881 |
. . . 4
⊢ 𝐵 ∈ V |
44 | 43 | a1i 11 |
. . 3
⊢ (𝐾 ∈ DivRing → 𝐵 ∈ V) |
45 | 37, 39, 40, 44 | qsalrel 38676 |
. 2
⊢ (𝐾 ∈ DivRing → (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠
‘𝑊)𝑦))}) = {𝐵}) |
46 | 8, 16, 45 | 3eqtrd 2837 |
1
⊢ (𝐾 ∈ DivRing →
(0ℙ𝕣𝕠𝕛n𝐾) = {𝐵}) |