Step |
Hyp |
Ref |
Expression |
1 |
|
mat1dim.a |
⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 ) |
2 |
|
mat1dim.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
3 |
|
mat1dim.o |
⊢ 𝑂 = 〈 𝐸 , 𝐸 〉 |
4 |
|
snfi |
⊢ { 𝐸 } ∈ Fin |
5 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
6 |
5
|
adantr |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring ) |
7 |
1
|
matring |
⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring ) |
8 |
4 6 7
|
sylancr |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Ring ) |
9 |
1 2 3
|
mat1dimelbas |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑎 ∈ 𝐵 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ) |
10 |
1 2 3
|
mat1dimelbas |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑦 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) ) |
11 |
9 10
|
anbi12d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ↔ ( ∃ 𝑎 ∈ 𝐵 𝑥 = { 〈 𝑂 , 𝑎 〉 } ∧ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) ) ) |
12 |
5 11
|
sylan |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ↔ ( ∃ 𝑎 ∈ 𝐵 𝑥 = { 〈 𝑂 , 𝑎 〉 } ∧ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) ) ) |
13 |
|
simpll |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ CRing ) |
14 |
|
simprl |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 ) |
15 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 ) |
16 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
17 |
2 16
|
crngcom |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ) |
18 |
13 14 15 17
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ) |
19 |
18
|
opeq2d |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 〈 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) 〉 = 〈 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) 〉 ) |
20 |
19
|
sneqd |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → { 〈 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) 〉 } = { 〈 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) 〉 } ) |
21 |
5
|
anim1i |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ) |
22 |
1 2 3
|
mat1dimmul |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = { 〈 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) 〉 } ) |
23 |
21 22
|
sylan |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = { 〈 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) 〉 } ) |
24 |
|
pm3.22 |
⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) |
25 |
1 2 3
|
mat1dimmul |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) → ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) = { 〈 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) 〉 } ) |
26 |
21 24 25
|
syl2an |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) = { 〈 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) 〉 } ) |
27 |
20 23 26
|
3eqtr4d |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) |
28 |
27
|
expr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) ) |
29 |
28
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) → ( 𝑏 ∈ 𝐵 → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) ) |
30 |
29
|
imp |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ∧ 𝑏 ∈ 𝐵 ) → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) |
31 |
30
|
adantr |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) → ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) |
32 |
|
oveq12 |
⊢ ( ( 𝑥 = { 〈 𝑂 , 𝑎 〉 } ∧ 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) ) |
33 |
32
|
ad4ant24 |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( { 〈 𝑂 , 𝑎 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑏 〉 } ) ) |
34 |
|
oveq12 |
⊢ ( ( 𝑦 = { 〈 𝑂 , 𝑏 〉 } ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) |
35 |
34
|
expcom |
⊢ ( 𝑥 = { 〈 𝑂 , 𝑎 〉 } → ( 𝑦 = { 〈 𝑂 , 𝑏 〉 } → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) ) |
36 |
35
|
ad2antlr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑦 = { 〈 𝑂 , 𝑏 〉 } → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) ) |
37 |
36
|
imp |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { 〈 𝑂 , 𝑏 〉 } ( .r ‘ 𝐴 ) { 〈 𝑂 , 𝑎 〉 } ) ) |
38 |
31 33 37
|
3eqtr4d |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) |
39 |
38
|
rexlimdva2 |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { 〈 𝑂 , 𝑎 〉 } ) → ( ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑂 , 𝑏 〉 } → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) ) |
40 |
39
|
rexlimdva2 |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ 𝐵 𝑥 = { 〈 𝑂 , 𝑎 〉 } → ( ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑂 , 𝑏 〉 } → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) ) ) |
41 |
40
|
impd |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ( ∃ 𝑎 ∈ 𝐵 𝑥 = { 〈 𝑂 , 𝑎 〉 } ∧ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑂 , 𝑏 〉 } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) ) |
42 |
12 41
|
sylbid |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) ) |
43 |
42
|
ralrimivv |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) |
44 |
|
eqid |
⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) |
45 |
|
eqid |
⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 ) |
46 |
44 45
|
iscrng2 |
⊢ ( 𝐴 ∈ CRing ↔ ( 𝐴 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) ) |
47 |
8 43 46
|
sylanbrc |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ CRing ) |