Proof of Theorem mat1dimelbas
Step | Hyp | Ref
| Expression |
1 | | snfi 8038 |
. . . 4
⊢ {𝐸} ∈ Fin |
2 | | simpl 473 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) |
3 | | mat1dim.a |
. . . . . . 7
⊢ 𝐴 = ({𝐸} Mat 𝑅) |
4 | | mat1dim.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
5 | 3, 4 | matbas2 20227 |
. . . . . 6
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐵 ↑𝑚
({𝐸} × {𝐸})) = (Base‘𝐴)) |
6 | 5 | eqcomd 2628 |
. . . . 5
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝐴) = (𝐵 ↑𝑚
({𝐸} × {𝐸}))) |
7 | 6 | eleq2d 2687 |
. . . 4
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀 ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸})))) |
8 | 1, 2, 7 | sylancr 695 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀 ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸})))) |
9 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝑅)
∈ V |
10 | 4, 9 | eqeltri 2697 |
. . . 4
⊢ 𝐵 ∈ V |
11 | | snex 4908 |
. . . . . 6
⊢ {𝐸} ∈ V |
12 | 11, 11 | pm3.2i 471 |
. . . . 5
⊢ ({𝐸} ∈ V ∧ {𝐸} ∈ V) |
13 | | xpexg 6960 |
. . . . 5
⊢ (({𝐸} ∈ V ∧ {𝐸} ∈ V) → ({𝐸} × {𝐸}) ∈ V) |
14 | 12, 13 | mp1i 13 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) ∈ V) |
15 | | elmapg 7870 |
. . . 4
⊢ ((𝐵 ∈ V ∧ ({𝐸} × {𝐸}) ∈ V) → (𝑀 ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸})) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
16 | 10, 14, 15 | sylancr 695 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (𝐵 ↑𝑚 ({𝐸} × {𝐸})) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
17 | 8, 16 | bitrd 268 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
18 | | xpsng 6406 |
. . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) |
19 | 18 | anidms 677 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑉 → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) |
20 | 19 | adantl 482 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) |
21 | 20 | feq2d 6031 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ 𝑀:{〈𝐸, 𝐸〉}⟶𝐵)) |
22 | | opex 4932 |
. . . . . . 7
⊢
〈𝐸, 𝐸〉 ∈ V |
23 | 22 | fsn2 6403 |
. . . . . 6
⊢ (𝑀:{〈𝐸, 𝐸〉}⟶𝐵 ↔ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) |
24 | | risset 3062 |
. . . . . . . . . 10
⊢ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑟 = (𝑀‘〈𝐸, 𝐸〉)) |
25 | | eqcom 2629 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑀‘〈𝐸, 𝐸〉) ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟) |
26 | 25 | rexbii 3041 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
𝐵 𝑟 = (𝑀‘〈𝐸, 𝐸〉) ↔ ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟) |
27 | 24, 26 | sylbb 209 |
. . . . . . . . 9
⊢ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 → ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟) |
28 | 27 | ad2antrl 764 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟) |
29 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉})) |
30 | | opex 4932 |
. . . . . . . . . . . . . . 15
⊢
〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 ∈ V |
31 | | sneqbg 4374 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 ∈ V →
({〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
({〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉) |
33 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
〈𝐸, 𝐸〉 = 〈𝐸, 𝐸〉 |
34 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑟 ∈ V |
35 | 22, 34 | opth2 4949 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉 ↔ (〈𝐸, 𝐸〉 = 〈𝐸, 𝐸〉 ∧ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) |
36 | 33, 35 | mpbiran 953 |
. . . . . . . . . . . . . 14
⊢
(〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉 ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟) |
37 | 32, 36 | bitri 264 |
. . . . . . . . . . . . 13
⊢
({〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟) |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} → ({〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) |
39 | 29, 38 | bitrd 268 |
. . . . . . . . . . 11
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) |
40 | 39 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉}) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) |
41 | 40 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) |
42 | 41 | rexbidv 3052 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → (∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) |
43 | 28, 42 | mpbird 247 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉}) |
44 | 43 | ex 450 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉}) → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) |
45 | 23, 44 | syl5bi 232 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:{〈𝐸, 𝐸〉}⟶𝐵 → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) |
46 | 21, 45 | sylbid 230 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) |
47 | | f1o2sn 6408 |
. . . . . . . . 9
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})–1-1-onto→{𝑟}) |
48 | | f1of 6137 |
. . . . . . . . 9
⊢
({〈〈𝐸,
𝐸〉, 𝑟〉}:({𝐸} × {𝐸})–1-1-onto→{𝑟} → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶{𝑟}) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶{𝑟}) |
50 | 49 | adantll 750 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶{𝑟}) |
51 | | snssi 4339 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝐵 → {𝑟} ⊆ 𝐵) |
52 | 51 | adantl 482 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {𝑟} ⊆ 𝐵) |
53 | 50, 52 | fssd 6057 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶𝐵) |
54 | | feq1 6026 |
. . . . . 6
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶𝐵)) |
55 | 53, 54 | syl5ibrcom 237 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} → 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
56 | 55 | rexlimdva 3031 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} → 𝑀:({𝐸} × {𝐸})⟶𝐵)) |
57 | 46, 56 | impbid 202 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) |
58 | | mat1dim.o |
. . . . . . . . 9
⊢ 𝑂 = 〈𝐸, 𝐸〉 |
59 | 58 | eqcomi 2631 |
. . . . . . . 8
⊢
〈𝐸, 𝐸〉 = 𝑂 |
60 | 59 | opeq1i 4405 |
. . . . . . 7
⊢
〈〈𝐸, 𝐸〉, 𝑟〉 = 〈𝑂, 𝑟〉 |
61 | 60 | sneqi 4188 |
. . . . . 6
⊢
{〈〈𝐸,
𝐸〉, 𝑟〉} = {〈𝑂, 𝑟〉} |
62 | 61 | eqeq2i 2634 |
. . . . 5
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 𝑀 = {〈𝑂, 𝑟〉}) |
63 | 62 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 𝑀 = {〈𝑂, 𝑟〉})) |
64 | 63 | rexbidv 3052 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈𝑂, 𝑟〉})) |
65 | 57, 64 | bitrd 268 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈𝑂, 𝑟〉})) |
66 | 17, 65 | bitrd 268 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈𝑂, 𝑟〉})) |