Step |
Hyp |
Ref |
Expression |
1 |
|
madetsmelbas.p |
|- P = ( Base ` ( SymGrp ` N ) ) |
2 |
|
madetsmelbas.s |
|- S = ( pmSgn ` N ) |
3 |
|
madetsmelbas.y |
|- Y = ( ZRHom ` R ) |
4 |
|
madetsmelbas.a |
|- A = ( N Mat R ) |
5 |
|
madetsmelbas.b |
|- B = ( Base ` A ) |
6 |
|
madetsmelbas.g |
|- G = ( mulGrp ` R ) |
7 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
8 |
7
|
3ad2ant1 |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> R e. Ring ) |
9 |
4 5
|
matrcl |
|- ( M e. B -> ( N e. Fin /\ R e. _V ) ) |
10 |
9
|
simpld |
|- ( M e. B -> N e. Fin ) |
11 |
10
|
3ad2ant2 |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> N e. Fin ) |
12 |
|
simp3 |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> Q e. P ) |
13 |
1 2 3
|
zrhcopsgnelbas |
|- ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) e. ( Base ` R ) ) |
14 |
8 11 12 13
|
syl3anc |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( ( Y o. S ) ` Q ) e. ( Base ` R ) ) |
15 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
16 |
6 15
|
mgpbas |
|- ( Base ` R ) = ( Base ` G ) |
17 |
6
|
crngmgp |
|- ( R e. CRing -> G e. CMnd ) |
18 |
17
|
3ad2ant1 |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> G e. CMnd ) |
19 |
|
simp2 |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> M e. B ) |
20 |
4 5 1
|
matepm2cl |
|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( n M ( Q ` n ) ) e. ( Base ` R ) ) |
21 |
8 12 19 20
|
syl3anc |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> A. n e. N ( n M ( Q ` n ) ) e. ( Base ` R ) ) |
22 |
16 18 11 21
|
gsummptcl |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) e. ( Base ` R ) ) |
23 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
24 |
15 23
|
ringcl |
|- ( ( R e. Ring /\ ( ( Y o. S ) ` Q ) e. ( Base ` R ) /\ ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) e. ( Base ` R ) ) -> ( ( ( Y o. S ) ` Q ) ( .r ` R ) ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) ) e. ( Base ` R ) ) |
25 |
8 14 22 24
|
syl3anc |
|- ( ( R e. CRing /\ M e. B /\ Q e. P ) -> ( ( ( Y o. S ) ` Q ) ( .r ` R ) ( G gsum ( n e. N |-> ( n M ( Q ` n ) ) ) ) ) e. ( Base ` R ) ) |