Step |
Hyp |
Ref |
Expression |
1 |
|
chmatcl.a |
|- A = ( N Mat R ) |
2 |
|
chmatcl.b |
|- B = ( Base ` A ) |
3 |
|
chmatcl.p |
|- P = ( Poly1 ` R ) |
4 |
|
chmatcl.y |
|- Y = ( N Mat P ) |
5 |
|
chmatcl.x |
|- X = ( var1 ` R ) |
6 |
|
chmatcl.t |
|- T = ( N matToPolyMat R ) |
7 |
|
chmatcl.s |
|- .- = ( -g ` Y ) |
8 |
|
chmatcl.m |
|- .x. = ( .s ` Y ) |
9 |
|
chmatcl.1 |
|- .1. = ( 1r ` Y ) |
10 |
|
chmatcl.h |
|- H = ( ( X .x. .1. ) .- ( T ` M ) ) |
11 |
3 4
|
pmatring |
|- ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring ) |
12 |
|
ringgrp |
|- ( Y e. Ring -> Y e. Grp ) |
13 |
11 12
|
syl |
|- ( ( N e. Fin /\ R e. Ring ) -> Y e. Grp ) |
14 |
13
|
3adant3 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Grp ) |
15 |
3
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
16 |
15
|
anim2i |
|- ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring ) ) |
17 |
16
|
3adant3 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) ) |
18 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
19 |
5 3 18
|
vr1cl |
|- ( R e. Ring -> X e. ( Base ` P ) ) |
20 |
19
|
3ad2ant2 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> X e. ( Base ` P ) ) |
21 |
11
|
3adant3 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Ring ) |
22 |
|
eqid |
|- ( Base ` Y ) = ( Base ` Y ) |
23 |
22 9
|
ringidcl |
|- ( Y e. Ring -> .1. e. ( Base ` Y ) ) |
24 |
21 23
|
syl |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .1. e. ( Base ` Y ) ) |
25 |
18 4 22 8
|
matvscl |
|- ( ( ( N e. Fin /\ P e. Ring ) /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Y ) ) ) -> ( X .x. .1. ) e. ( Base ` Y ) ) |
26 |
17 20 24 25
|
syl12anc |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) ) |
27 |
6 1 2 3 4
|
mat2pmatbas |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) ) |
28 |
22 7
|
grpsubcl |
|- ( ( Y e. Grp /\ ( X .x. .1. ) e. ( Base ` Y ) /\ ( T ` M ) e. ( Base ` Y ) ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) ) |
29 |
14 26 27 28
|
syl3anc |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) ) |
30 |
10 29
|
eqeltrid |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> H e. ( Base ` Y ) ) |