Step | Hyp | Ref
| Expression |
1 | | snfi 8994 |
. . . 4
⊢ {𝐸} ∈ Fin |
2 | | simpl 484 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) |
3 | | mat1dim.a |
. . . . . . 7
⊢ 𝐴 = ({𝐸} Mat 𝑅) |
4 | | mat1dim.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
5 | 3, 4 | matbas2 21793 |
. . . . . 6
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐵 ↑m ({𝐸} × {𝐸})) = (Base‘𝐴)) |
6 | 5 | eqcomd 2739 |
. . . . 5
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝐴) = (𝐵 ↑m ({𝐸} × {𝐸}))) |
7 | 6 | eleq2d 2820 |
. . . 4
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})))) |
8 | 1, 2, 7 | sylancr 588 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})))) |
9 | 4 | fvexi 6860 |
. . . 4
⊢ 𝐵 ∈ V |
10 | | snex 5392 |
. . . . . 6
⊢ {𝐸} ∈ V |
11 | 10, 10 | pm3.2i 472 |
. . . . 5
⊢ ({𝐸} ∈ V ∧ {𝐸} ∈ V) |
12 | | xpexg 7688 |
. . . . 5
⊢ (({𝐸} ∈ V ∧ {𝐸} ∈ V) → ({𝐸} × {𝐸}) ∈ V) |
13 | 11, 12 | mp1i 13 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) ∈ V) |
14 | | elmapg 8784 |
. . . 4
⊢ ((𝐵 ∈ V ∧ ({𝐸} × {𝐸}) ∈ V) → (𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
15 | 9, 13, 14 | sylancr 588 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
16 | 8, 15 | bitrd 279 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
17 | | xpsng 7089 |
. . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {⟨𝐸, 𝐸⟩}) |
18 | 17 | anidms 568 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑉 → ({𝐸} × {𝐸}) = {⟨𝐸, 𝐸⟩}) |
19 | 18 | adantl 483 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {⟨𝐸, 𝐸⟩}) |
20 | 19 | feq2d 6658 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ 𝑀:{⟨𝐸, 𝐸⟩}⟶𝐵)) |
21 | | opex 5425 |
. . . . . . 7
⊢
⟨𝐸, 𝐸⟩ ∈ V |
22 | 21 | fsn2 7086 |
. . . . . 6
⊢ (𝑀:{⟨𝐸, 𝐸⟩}⟶𝐵 ↔ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩})) |
23 | | risset 3220 |
. . . . . . . . . 10
⊢ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑟 = (𝑀‘⟨𝐸, 𝐸⟩)) |
24 | | eqcom 2740 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑀‘⟨𝐸, 𝐸⟩) ↔ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟) |
25 | 24 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
𝐵 𝑟 = (𝑀‘⟨𝐸, 𝐸⟩) ↔ ∃𝑟 ∈ 𝐵 (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟) |
26 | 23, 25 | sylbb 218 |
. . . . . . . . 9
⊢ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 → ∃𝑟 ∈ 𝐵 (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟) |
27 | 26 | ad2antrl 727 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩})) → ∃𝑟 ∈ 𝐵 (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟) |
28 | | eqeq1 2737 |
. . . . . . . . . . . 12
⊢ (𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩} → (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩} = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩})) |
29 | | opex 5425 |
. . . . . . . . . . . . . 14
⊢
⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩ ∈ V |
30 | | sneqbg 4805 |
. . . . . . . . . . . . . 14
⊢
(⟨⟨𝐸,
𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩ ∈ V →
({⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩} = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ ⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩ = ⟨⟨𝐸, 𝐸⟩, 𝑟⟩)) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({⟨⟨𝐸,
𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩} = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ ⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩ = ⟨⟨𝐸, 𝐸⟩, 𝑟⟩) |
32 | | eqid 2733 |
. . . . . . . . . . . . . 14
⊢
⟨𝐸, 𝐸⟩ = ⟨𝐸, 𝐸⟩ |
33 | | vex 3451 |
. . . . . . . . . . . . . . 15
⊢ 𝑟 ∈ V |
34 | 21, 33 | opth2 5441 |
. . . . . . . . . . . . . 14
⊢
(⟨⟨𝐸,
𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩ = ⟨⟨𝐸, 𝐸⟩, 𝑟⟩ ↔ (⟨𝐸, 𝐸⟩ = ⟨𝐸, 𝐸⟩ ∧ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟)) |
35 | 32, 34 | mpbiran 708 |
. . . . . . . . . . . . 13
⊢
(⟨⟨𝐸,
𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩ = ⟨⟨𝐸, 𝐸⟩, 𝑟⟩ ↔ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟) |
36 | 31, 35 | bitri 275 |
. . . . . . . . . . . 12
⊢
({⟨⟨𝐸,
𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩} = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟) |
37 | 28, 36 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩} → (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟)) |
38 | 37 | adantl 483 |
. . . . . . . . . 10
⊢ (((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩}) → (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟)) |
39 | 38 | adantl 483 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩})) → (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟)) |
40 | 39 | rexbidv 3172 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩})) → (∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ ∃𝑟 ∈ 𝐵 (𝑀‘⟨𝐸, 𝐸⟩) = 𝑟)) |
41 | 27, 40 | mpbird 257 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩})) → ∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}) |
42 | 41 | ex 414 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (((𝑀‘⟨𝐸, 𝐸⟩) ∈ 𝐵 ∧ 𝑀 = {⟨⟨𝐸, 𝐸⟩, (𝑀‘⟨𝐸, 𝐸⟩)⟩}) → ∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩})) |
43 | 22, 42 | biimtrid 241 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:{⟨𝐸, 𝐸⟩}⟶𝐵 → ∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩})) |
44 | 20, 43 | sylbid 239 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 → ∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩})) |
45 | | f1o2sn 7092 |
. . . . . . . . 9
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵) → {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})–1-1-onto→{𝑟}) |
46 | | f1of 6788 |
. . . . . . . . 9
⊢
({⟨⟨𝐸,
𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})–1-1-onto→{𝑟} → {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})⟶{𝑟}) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵) → {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})⟶{𝑟}) |
48 | 47 | adantll 713 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})⟶{𝑟}) |
49 | | snssi 4772 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝐵 → {𝑟} ⊆ 𝐵) |
50 | 49 | adantl 483 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {𝑟} ⊆ 𝐵) |
51 | 48, 50 | fssd 6690 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})⟶𝐵) |
52 | | feq1 6653 |
. . . . . 6
⊢ (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ {⟨⟨𝐸, 𝐸⟩, 𝑟⟩}:({𝐸} × {𝐸})⟶𝐵)) |
53 | 51, 52 | syl5ibrcom 247 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} → 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
54 | 53 | rexlimdva 3149 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} → 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
55 | 44, 54 | impbid 211 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩})) |
56 | | mat1dim.o |
. . . . . . . . 9
⊢ 𝑂 = ⟨𝐸, 𝐸⟩ |
57 | 56 | eqcomi 2742 |
. . . . . . . 8
⊢
⟨𝐸, 𝐸⟩ = 𝑂 |
58 | 57 | opeq1i 4837 |
. . . . . . 7
⊢
⟨⟨𝐸, 𝐸⟩, 𝑟⟩ = ⟨𝑂, 𝑟⟩ |
59 | 58 | sneqi 4601 |
. . . . . 6
⊢
{⟨⟨𝐸,
𝐸⟩, 𝑟⟩} = {⟨𝑂, 𝑟⟩} |
60 | 59 | eqeq2i 2746 |
. . . . 5
⊢ (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ 𝑀 = {⟨𝑂, 𝑟⟩}) |
61 | 60 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ 𝑀 = {⟨𝑂, 𝑟⟩})) |
62 | 61 | rexbidv 3172 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∃𝑟 ∈ 𝐵 𝑀 = {⟨⟨𝐸, 𝐸⟩, 𝑟⟩} ↔ ∃𝑟 ∈ 𝐵 𝑀 = {⟨𝑂, 𝑟⟩})) |
63 | 55, 62 | bitrd 279 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑀 = {⟨𝑂, 𝑟⟩})) |
64 | 16, 63 | bitrd 279 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ ∃𝑟 ∈ 𝐵 𝑀 = {⟨𝑂, 𝑟⟩})) |