Step | Hyp | Ref
| Expression |
1 | | snfi 8834 |
. . 3
⊢ {𝐸} ∈ Fin |
2 | | crngring 19795 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
3 | 2 | adantr 481 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) |
4 | | mat1dim.a |
. . . 4
⊢ 𝐴 = ({𝐸} Mat 𝑅) |
5 | 4 | matring 21592 |
. . 3
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
6 | 1, 3, 5 | sylancr 587 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → 𝐴 ∈ Ring) |
7 | | mat1dim.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
8 | | mat1dim.o |
. . . . . . 7
⊢ 𝑂 = 〈𝐸, 𝐸〉 |
9 | 4, 7, 8 | mat1dimelbas 21620 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑥 ∈ (Base‘𝐴) ↔ ∃𝑎 ∈ 𝐵 𝑥 = {〈𝑂, 𝑎〉})) |
10 | 4, 7, 8 | mat1dimelbas 21620 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑦 ∈ (Base‘𝐴) ↔ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑂, 𝑏〉})) |
11 | 9, 10 | anbi12d 631 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) ↔ (∃𝑎 ∈ 𝐵 𝑥 = {〈𝑂, 𝑎〉} ∧ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑂, 𝑏〉}))) |
12 | 2, 11 | sylan 580 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) ↔ (∃𝑎 ∈ 𝐵 𝑥 = {〈𝑂, 𝑎〉} ∧ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑂, 𝑏〉}))) |
13 | | simpll 764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ CRing) |
14 | | simprl 768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
15 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
16 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) |
17 | 7, 16 | crngcom 19801 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑅)𝑏) = (𝑏(.r‘𝑅)𝑎)) |
18 | 13, 14, 15, 17 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(.r‘𝑅)𝑏) = (𝑏(.r‘𝑅)𝑎)) |
19 | 18 | opeq2d 4811 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 〈𝑂, (𝑎(.r‘𝑅)𝑏)〉 = 〈𝑂, (𝑏(.r‘𝑅)𝑎)〉) |
20 | 19 | sneqd 4573 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → {〈𝑂, (𝑎(.r‘𝑅)𝑏)〉} = {〈𝑂, (𝑏(.r‘𝑅)𝑎)〉}) |
21 | 2 | anim1i 615 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → (𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉)) |
22 | 4, 7, 8 | mat1dimmul 21625 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = {〈𝑂, (𝑎(.r‘𝑅)𝑏)〉}) |
23 | 21, 22 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = {〈𝑂, (𝑎(.r‘𝑅)𝑏)〉}) |
24 | | pm3.22 460 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) |
25 | 4, 7, 8 | mat1dimmul 21625 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) → ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉}) = {〈𝑂, (𝑏(.r‘𝑅)𝑎)〉}) |
26 | 21, 24, 25 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉}) = {〈𝑂, (𝑏(.r‘𝑅)𝑎)〉}) |
27 | 20, 23, 26 | 3eqtr4d 2788 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉})) |
28 | 27 | expr 457 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉}))) |
29 | 28 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) → (𝑏 ∈ 𝐵 → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉}))) |
30 | 29 | imp 407 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) ∧ 𝑏 ∈ 𝐵) → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉})) |
31 | 30 | adantr 481 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = {〈𝑂, 𝑏〉}) → ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉}) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉})) |
32 | | oveq12 7284 |
. . . . . . . . 9
⊢ ((𝑥 = {〈𝑂, 𝑎〉} ∧ 𝑦 = {〈𝑂, 𝑏〉}) → (𝑥(.r‘𝐴)𝑦) = ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉})) |
33 | 32 | ad4ant24 751 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = {〈𝑂, 𝑏〉}) → (𝑥(.r‘𝐴)𝑦) = ({〈𝑂, 𝑎〉} (.r‘𝐴){〈𝑂, 𝑏〉})) |
34 | | oveq12 7284 |
. . . . . . . . . . 11
⊢ ((𝑦 = {〈𝑂, 𝑏〉} ∧ 𝑥 = {〈𝑂, 𝑎〉}) → (𝑦(.r‘𝐴)𝑥) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉})) |
35 | 34 | expcom 414 |
. . . . . . . . . 10
⊢ (𝑥 = {〈𝑂, 𝑎〉} → (𝑦 = {〈𝑂, 𝑏〉} → (𝑦(.r‘𝐴)𝑥) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉}))) |
36 | 35 | ad2antlr 724 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) ∧ 𝑏 ∈ 𝐵) → (𝑦 = {〈𝑂, 𝑏〉} → (𝑦(.r‘𝐴)𝑥) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉}))) |
37 | 36 | imp 407 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = {〈𝑂, 𝑏〉}) → (𝑦(.r‘𝐴)𝑥) = ({〈𝑂, 𝑏〉} (.r‘𝐴){〈𝑂, 𝑎〉})) |
38 | 31, 33, 37 | 3eqtr4d 2788 |
. . . . . . 7
⊢
((((((𝑅 ∈ CRing
∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = {〈𝑂, 𝑏〉}) → (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥)) |
39 | 38 | rexlimdva2 3216 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = {〈𝑂, 𝑎〉}) → (∃𝑏 ∈ 𝐵 𝑦 = {〈𝑂, 𝑏〉} → (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
40 | 39 | rexlimdva2 3216 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → (∃𝑎 ∈ 𝐵 𝑥 = {〈𝑂, 𝑎〉} → (∃𝑏 ∈ 𝐵 𝑦 = {〈𝑂, 𝑏〉} → (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥)))) |
41 | 40 | impd 411 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → ((∃𝑎 ∈ 𝐵 𝑥 = {〈𝑂, 𝑎〉} ∧ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑂, 𝑏〉}) → (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
42 | 12, 41 | sylbid 239 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) → (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
43 | 42 | ralrimivv 3122 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)(𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥)) |
44 | | eqid 2738 |
. . 3
⊢
(Base‘𝐴) =
(Base‘𝐴) |
45 | | eqid 2738 |
. . 3
⊢
(.r‘𝐴) = (.r‘𝐴) |
46 | 44, 45 | iscrng2 19802 |
. 2
⊢ (𝐴 ∈ CRing ↔ (𝐴 ∈ Ring ∧ ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)(𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
47 | 6, 43, 46 | sylanbrc 583 |
1
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → 𝐴 ∈ CRing) |