Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. 2
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
2 | | 0prjspnrel.b |
. . . 4
⊢ 𝐵 = ((Base‘𝑊) ∖
{(0g‘𝑊)}) |
3 | | 0prjspnrel.w |
. . . 4
⊢ 𝑊 = (𝐾 freeLMod (0...0)) |
4 | | 0prjspnrel.1 |
. . . 4
⊢ 1 = ((𝐾 unitVec
(0...0))‘0) |
5 | 2, 3, 4 | 0prjspnlem 40078 |
. . 3
⊢ (𝐾 ∈ DivRing → 1 ∈ 𝐵) |
6 | 5 | adantr 484 |
. 2
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 1 ∈ 𝐵) |
7 | | ovexd 7218 |
. . . . . 6
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → (0...0) ∈ V) |
8 | | difss 4032 |
. . . . . . . . 9
⊢
((Base‘𝑊)
∖ {(0g‘𝑊)}) ⊆ (Base‘𝑊) |
9 | 2, 8 | eqsstri 3921 |
. . . . . . . 8
⊢ 𝐵 ⊆ (Base‘𝑊) |
10 | 9 | sseli 3883 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘𝑊)) |
11 | 10 | adantl 485 |
. . . . . 6
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ (Base‘𝑊)) |
12 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
13 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
14 | 3, 12, 13 | frlmbasf 20589 |
. . . . . 6
⊢ (((0...0)
∈ V ∧ 𝑋 ∈
(Base‘𝑊)) →
𝑋:(0...0)⟶(Base‘𝐾)) |
15 | 7, 11, 14 | syl2anc 587 |
. . . . 5
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋:(0...0)⟶(Base‘𝐾)) |
16 | | c0ex 10726 |
. . . . . . . 8
⊢ 0 ∈
V |
17 | 16 | snid 4562 |
. . . . . . 7
⊢ 0 ∈
{0} |
18 | | fz0sn 13111 |
. . . . . . 7
⊢ (0...0) =
{0} |
19 | 17, 18 | eleqtrri 2833 |
. . . . . 6
⊢ 0 ∈
(0...0) |
20 | 19 | a1i 11 |
. . . . 5
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 0 ∈ (0...0)) |
21 | 15, 20 | ffvelrnd 6875 |
. . . 4
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → (𝑋‘0) ∈ (Base‘𝐾)) |
22 | | sneq 4536 |
. . . . . . 7
⊢ (𝑛 = (𝑋‘0) → {𝑛} = {(𝑋‘0)}) |
23 | 22 | xpeq2d 5565 |
. . . . . 6
⊢ (𝑛 = (𝑋‘0) → ((0...0) × {𝑛}) = ((0...0) × {(𝑋‘0)})) |
24 | 23 | eqeq2d 2750 |
. . . . 5
⊢ (𝑛 = (𝑋‘0) → (𝑋 = ((0...0) × {𝑛}) ↔ 𝑋 = ((0...0) × {(𝑋‘0)}))) |
25 | 24 | adantl 485 |
. . . 4
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 = (𝑋‘0)) → (𝑋 = ((0...0) × {𝑛}) ↔ 𝑋 = ((0...0) × {(𝑋‘0)}))) |
26 | 3, 12, 13 | frlmbasmap 20588 |
. . . . . 6
⊢ (((0...0)
∈ V ∧ 𝑋 ∈
(Base‘𝑊)) →
𝑋 ∈ ((Base‘𝐾) ↑m
(0...0))) |
27 | 7, 11, 26 | syl2anc 587 |
. . . . 5
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ ((Base‘𝐾) ↑m
(0...0))) |
28 | | fvex 6700 |
. . . . . 6
⊢
(Base‘𝐾)
∈ V |
29 | 18, 28, 16 | mapsnconst 8515 |
. . . . 5
⊢ (𝑋 ∈ ((Base‘𝐾) ↑m (0...0))
→ 𝑋 = ((0...0) ×
{(𝑋‘0)})) |
30 | 27, 29 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 = ((0...0) × {(𝑋‘0)})) |
31 | 21, 25, 30 | rspcedvd 3532 |
. . 3
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → ∃𝑛 ∈ (Base‘𝐾)𝑋 = ((0...0) × {𝑛})) |
32 | | simprl 771 |
. . . . 5
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑛 ∈ (Base‘𝐾) ∧ 𝑋 = ((0...0) × {𝑛}))) → 𝑛 ∈ (Base‘𝐾)) |
33 | | 0prjspnrel.s |
. . . . 5
⊢ 𝑆 = (Base‘𝐾) |
34 | 32, 33 | eleqtrrdi 2845 |
. . . 4
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑛 ∈ (Base‘𝐾) ∧ 𝑋 = ((0...0) × {𝑛}))) → 𝑛 ∈ 𝑆) |
35 | | oveq1 7190 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑚 · 1 ) = (𝑛 · 1 )) |
36 | 35 | eqeq2d 2750 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑋 = (𝑚 · 1 ) ↔ 𝑋 = (𝑛 · 1 ))) |
37 | 36 | adantl 485 |
. . . 4
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑛 ∈ (Base‘𝐾) ∧ 𝑋 = ((0...0) × {𝑛}))) ∧ 𝑚 = 𝑛) → (𝑋 = (𝑚 · 1 ) ↔ 𝑋 = (𝑛 · 1 ))) |
38 | | ovexd 7218 |
. . . . . . . . 9
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (0...0) ∈ V) |
39 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 𝑛 ∈ (Base‘𝐾)) |
40 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 1 ∈ 𝐵) |
41 | 9, 40 | sseldi 3885 |
. . . . . . . . 9
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 1 ∈ (Base‘𝑊)) |
42 | | 0prjspnrel.x |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑊) |
43 | | eqid 2739 |
. . . . . . . . 9
⊢
(.r‘𝐾) = (.r‘𝐾) |
44 | 3, 13, 12, 38, 39, 41, 42, 43 | frlmvscafval 20595 |
. . . . . . . 8
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (𝑛 · 1 ) = (((0...0) ×
{𝑛}) ∘f
(.r‘𝐾)
1
)) |
45 | 3, 12, 13 | frlmbasf 20589 |
. . . . . . . . . . 11
⊢ (((0...0)
∈ V ∧ 1 ∈ (Base‘𝑊)) → 1
:(0...0)⟶(Base‘𝐾)) |
46 | 38, 41, 45 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 1
:(0...0)⟶(Base‘𝐾)) |
47 | | drngring 19641 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ DivRing → 𝐾 ∈ Ring) |
48 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝐾) = (1r‘𝐾) |
49 | 12, 48 | ringidcl 19453 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Ring →
(1r‘𝐾)
∈ (Base‘𝐾)) |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ DivRing →
(1r‘𝐾)
∈ (Base‘𝐾)) |
51 | 50 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (1r‘𝐾) ∈ (Base‘𝐾)) |
52 | 51 | snssd 4707 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → {(1r‘𝐾)} ⊆ (Base‘𝐾)) |
53 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ (0...0) → 1 = ((𝐾 unitVec
(0...0))‘0)) |
54 | | elfz1eq 13022 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ (0...0) → 𝑑 = 0) |
55 | 53, 54 | fveq12d 6694 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ (0...0) → ( 1 ‘𝑑) = (((𝐾 unitVec
(0...0))‘0)‘0)) |
56 | 55 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → ( 1 ‘𝑑) = (((𝐾 unitVec
(0...0))‘0)‘0)) |
57 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 unitVec (0...0)) = (𝐾 unitVec
(0...0)) |
58 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → 𝐾 ∈ DivRing) |
59 | | ovexd 7218 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → (0...0) ∈
V) |
60 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → 0 ∈
(0...0)) |
61 | 57, 58, 59, 60, 48 | uvcvv1 20618 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → (((𝐾 unitVec (0...0))‘0)‘0) =
(1r‘𝐾)) |
62 | | fvex 6700 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 unitVec
(0...0))‘0)‘0) ∈ V |
63 | 62 | elsn 4541 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 unitVec
(0...0))‘0)‘0) ∈ {(1r‘𝐾)} ↔ (((𝐾 unitVec (0...0))‘0)‘0) =
(1r‘𝐾)) |
64 | 61, 63 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → (((𝐾 unitVec (0...0))‘0)‘0) ∈
{(1r‘𝐾)}) |
65 | 56, 64 | eqeltrd 2834 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑑 ∈ (0...0)) → ( 1 ‘𝑑) ∈ {(1r‘𝐾)}) |
66 | 65 | ralrimiva 3097 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → ∀𝑑 ∈ (0...0)( 1 ‘𝑑) ∈ {(1r‘𝐾)}) |
67 | | frnssb 6908 |
. . . . . . . . . . 11
⊢
(({(1r‘𝐾)} ⊆ (Base‘𝐾) ∧ ∀𝑑 ∈ (0...0)( 1 ‘𝑑) ∈ {(1r‘𝐾)}) → ( 1
:(0...0)⟶(Base‘𝐾) ↔ 1
:(0...0)⟶{(1r‘𝐾)})) |
68 | 52, 66, 67 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → ( 1
:(0...0)⟶(Base‘𝐾) ↔ 1
:(0...0)⟶{(1r‘𝐾)})) |
69 | 46, 68 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 1
:(0...0)⟶{(1r‘𝐾)}) |
70 | | vex 3404 |
. . . . . . . . . 10
⊢ 𝑛 ∈ V |
71 | 70 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 𝑛 ∈ V) |
72 | | elsni 4543 |
. . . . . . . . . . 11
⊢ (𝑐 ∈
{(1r‘𝐾)}
→ 𝑐 =
(1r‘𝐾)) |
73 | 72 | oveq2d 7199 |
. . . . . . . . . 10
⊢ (𝑐 ∈
{(1r‘𝐾)}
→ (𝑛(.r‘𝐾)𝑐) = (𝑛(.r‘𝐾)(1r‘𝐾))) |
74 | 47 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → 𝐾 ∈ Ring) |
75 | 12, 43, 48 | ringridm 19457 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Ring ∧ 𝑛 ∈ (Base‘𝐾)) → (𝑛(.r‘𝐾)(1r‘𝐾)) = 𝑛) |
76 | 74, 39, 75 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (𝑛(.r‘𝐾)(1r‘𝐾)) = 𝑛) |
77 | 73, 76 | sylan9eqr 2796 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) ∧ 𝑐 ∈ {(1r‘𝐾)}) → (𝑛(.r‘𝐾)𝑐) = 𝑛) |
78 | 38, 69, 71, 71, 77 | caofid2 7471 |
. . . . . . . 8
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (((0...0) × {𝑛}) ∘f
(.r‘𝐾)
1 ) =
((0...0) × {𝑛})) |
79 | 44, 78 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (𝑛 · 1 ) = ((0...0) ×
{𝑛})) |
80 | 79 | eqeq2d 2750 |
. . . . . 6
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (𝑋 = (𝑛 · 1 ) ↔ 𝑋 = ((0...0) × {𝑛}))) |
81 | 80 | biimprd 251 |
. . . . 5
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ (Base‘𝐾)) → (𝑋 = ((0...0) × {𝑛}) → 𝑋 = (𝑛 · 1 ))) |
82 | 81 | impr 458 |
. . . 4
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑛 ∈ (Base‘𝐾) ∧ 𝑋 = ((0...0) × {𝑛}))) → 𝑋 = (𝑛 · 1 )) |
83 | 34, 37, 82 | rspcedvd 3532 |
. . 3
⊢ (((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑛 ∈ (Base‘𝐾) ∧ 𝑋 = ((0...0) × {𝑛}))) → ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 1 )) |
84 | 31, 83 | rexlimddv 3202 |
. 2
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 1 )) |
85 | | 0prjspnrel.e |
. . 3
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} |
86 | 85 | prjsprel 40061 |
. 2
⊢ (𝑋 ∼ 1 ↔ ((𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 1 ))) |
87 | 1, 6, 84, 86 | syl21anbrc 1345 |
1
⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∼ 1 ) |