Step | Hyp | Ref
| Expression |
1 | | hash1snb 13068 |
. . 3
⊢ (𝑁 ∈ 𝑉 → ((#‘𝑁) = 1 ↔ ∃𝑒 𝑁 = {𝑒})) |
2 | | simpr 476 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (Base‘({𝑒} Mat 𝑅))) → 𝑀 ∈ (Base‘({𝑒} Mat 𝑅))) |
3 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑒 ∈ V |
4 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ({𝑒} Mat 𝑅) = ({𝑒} Mat 𝑅) |
5 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | | eqid 2610 |
. . . . . . . . . . 11
⊢
〈𝑒, 𝑒〉 = 〈𝑒, 𝑒〉 |
7 | 4, 5, 6 | mat1dimelbas 20096 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑒 ∈ V) → (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) ↔ ∃𝑐 ∈ (Base‘𝑅)𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉})) |
8 | 3, 7 | mpan2 703 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) ↔ ∃𝑐 ∈ (Base‘𝑅)𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉})) |
9 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉}) → 𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉}) |
10 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ (Base‘𝑅) → 𝑒 ∈ V) |
11 | 4, 5, 6 | mat1dimid 20099 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑒 ∈ V) →
(1r‘({𝑒}
Mat 𝑅)) =
{〈〈𝑒, 𝑒〉,
(1r‘𝑅)〉}) |
12 | 10, 11 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) →
(1r‘({𝑒}
Mat 𝑅)) =
{〈〈𝑒, 𝑒〉,
(1r‘𝑅)〉}) |
13 | 12 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅))) = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅)){〈〈𝑒, 𝑒〉, (1r‘𝑅)〉})) |
14 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
15 | 14, 3 | jctir 559 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝑒 ∈ V)) |
16 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → 𝑐 ∈ (Base‘𝑅)) |
17 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(1r‘𝑅) = (1r‘𝑅) |
18 | 5, 17 | ringidcl 18391 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) →
(1r‘𝑅)
∈ (Base‘𝑅)) |
20 | 4, 5, 6 | mat1dimscm 20100 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝑒 ∈ V) ∧ (𝑐 ∈ (Base‘𝑅) ∧
(1r‘𝑅)
∈ (Base‘𝑅)))
→ (𝑐(
·𝑠 ‘({𝑒} Mat 𝑅)){〈〈𝑒, 𝑒〉, (1r‘𝑅)〉}) = {〈〈𝑒, 𝑒〉, (𝑐(.r‘𝑅)(1r‘𝑅))〉}) |
21 | 15, 16, 19, 20 | syl12anc 1316 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → (𝑐( ·𝑠
‘({𝑒} Mat 𝑅)){〈〈𝑒, 𝑒〉, (1r‘𝑅)〉}) = {〈〈𝑒, 𝑒〉, (𝑐(.r‘𝑅)(1r‘𝑅))〉}) |
22 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) |
23 | 5, 22, 17 | ringridm 18395 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → (𝑐(.r‘𝑅)(1r‘𝑅)) = 𝑐) |
24 | 23 | opeq2d 4347 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → 〈〈𝑒, 𝑒〉, (𝑐(.r‘𝑅)(1r‘𝑅))〉 = 〈〈𝑒, 𝑒〉, 𝑐〉) |
25 | 24 | sneqd 4137 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → {〈〈𝑒, 𝑒〉, (𝑐(.r‘𝑅)(1r‘𝑅))〉} = {〈〈𝑒, 𝑒〉, 𝑐〉}) |
26 | 13, 21, 25 | 3eqtrrd 2649 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → {〈〈𝑒, 𝑒〉, 𝑐〉} = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅)))) |
27 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉}) → {〈〈𝑒, 𝑒〉, 𝑐〉} = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅)))) |
28 | 9, 27 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉}) → 𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅)))) |
29 | 28 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅)) → (𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉} → 𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅))))) |
30 | 29 | reximdva 3000 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(∃𝑐 ∈
(Base‘𝑅)𝑀 = {〈〈𝑒, 𝑒〉, 𝑐〉} → ∃𝑐 ∈ (Base‘𝑅)𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅))))) |
31 | 8, 30 | sylbid 229 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) → ∃𝑐 ∈ (Base‘𝑅)𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅))))) |
32 | 31 | imp 444 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (Base‘({𝑒} Mat 𝑅))) → ∃𝑐 ∈ (Base‘𝑅)𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅)))) |
33 | | snfi 7923 |
. . . . . . . 8
⊢ {𝑒} ∈ Fin |
34 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (Base‘({𝑒} Mat 𝑅))) → 𝑅 ∈ Ring) |
35 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘({𝑒} Mat
𝑅)) = (Base‘({𝑒} Mat 𝑅)) |
36 | | eqid 2610 |
. . . . . . . . 9
⊢
(1r‘({𝑒} Mat 𝑅)) = (1r‘({𝑒} Mat 𝑅)) |
37 | | eqid 2610 |
. . . . . . . . 9
⊢ (
·𝑠 ‘({𝑒} Mat 𝑅)) = ( ·𝑠
‘({𝑒} Mat 𝑅)) |
38 | | eqid 2610 |
. . . . . . . . 9
⊢ ({𝑒} ScMat 𝑅) = ({𝑒} ScMat 𝑅) |
39 | 5, 4, 35, 36, 37, 38 | scmatel 20130 |
. . . . . . . 8
⊢ (({𝑒} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ ({𝑒} ScMat 𝑅) ↔ (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) ∧ ∃𝑐 ∈ (Base‘𝑅)𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅)))))) |
40 | 33, 34, 39 | sylancr 694 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (Base‘({𝑒} Mat 𝑅))) → (𝑀 ∈ ({𝑒} ScMat 𝑅) ↔ (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) ∧ ∃𝑐 ∈ (Base‘𝑅)𝑀 = (𝑐( ·𝑠
‘({𝑒} Mat 𝑅))(1r‘({𝑒} Mat 𝑅)))))) |
41 | 2, 32, 40 | mpbir2and 959 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (Base‘({𝑒} Mat 𝑅))) → 𝑀 ∈ ({𝑒} ScMat 𝑅)) |
42 | 41 | ex 449 |
. . . . 5
⊢ (𝑅 ∈ Ring → (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) → 𝑀 ∈ ({𝑒} ScMat 𝑅))) |
43 | | mat1scmat.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐴) |
44 | | mat1scmat.a |
. . . . . . . . . 10
⊢ 𝐴 = (𝑁 Mat 𝑅) |
45 | 44 | fveq2i 6106 |
. . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
46 | 43, 45 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
47 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑁 = {𝑒} → (𝑁 Mat 𝑅) = ({𝑒} Mat 𝑅)) |
48 | 47 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑁 = {𝑒} → (Base‘(𝑁 Mat 𝑅)) = (Base‘({𝑒} Mat 𝑅))) |
49 | 46, 48 | syl5eq 2656 |
. . . . . . 7
⊢ (𝑁 = {𝑒} → 𝐵 = (Base‘({𝑒} Mat 𝑅))) |
50 | 49 | eleq2d 2673 |
. . . . . 6
⊢ (𝑁 = {𝑒} → (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘({𝑒} Mat 𝑅)))) |
51 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑁 = {𝑒} → (𝑁 ScMat 𝑅) = ({𝑒} ScMat 𝑅)) |
52 | 51 | eleq2d 2673 |
. . . . . 6
⊢ (𝑁 = {𝑒} → (𝑀 ∈ (𝑁 ScMat 𝑅) ↔ 𝑀 ∈ ({𝑒} ScMat 𝑅))) |
53 | 50, 52 | imbi12d 333 |
. . . . 5
⊢ (𝑁 = {𝑒} → ((𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅)) ↔ (𝑀 ∈ (Base‘({𝑒} Mat 𝑅)) → 𝑀 ∈ ({𝑒} ScMat 𝑅)))) |
54 | 42, 53 | syl5ibr 235 |
. . . 4
⊢ (𝑁 = {𝑒} → (𝑅 ∈ Ring → (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅)))) |
55 | 54 | exlimiv 1845 |
. . 3
⊢
(∃𝑒 𝑁 = {𝑒} → (𝑅 ∈ Ring → (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅)))) |
56 | 1, 55 | syl6bi 242 |
. 2
⊢ (𝑁 ∈ 𝑉 → ((#‘𝑁) = 1 → (𝑅 ∈ Ring → (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅))))) |
57 | 56 | 3imp 1249 |
1
⊢ ((𝑁 ∈ 𝑉 ∧ (#‘𝑁) = 1 ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅))) |