Step |
Hyp |
Ref |
Expression |
1 |
|
pwsmulg.y |
|- Y = ( R ^s I ) |
2 |
|
pwsmulg.b |
|- B = ( Base ` Y ) |
3 |
|
pwsmulg.s |
|- .xb = ( .g ` Y ) |
4 |
|
pwsmulg.t |
|- .x. = ( .g ` R ) |
5 |
|
simpll |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> R e. Mnd ) |
6 |
|
simplr |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> I e. V ) |
7 |
|
simpr3 |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> A e. I ) |
8 |
1 2
|
pwspjmhm |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) ) |
9 |
5 6 7 8
|
syl3anc |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) ) |
10 |
|
simpr1 |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> N e. NN0 ) |
11 |
|
simpr2 |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> X e. B ) |
12 |
2 3 4
|
mhmmulg |
|- ( ( ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) /\ N e. NN0 /\ X e. B ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) ) |
13 |
9 10 11 12
|
syl3anc |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) ) |
14 |
1
|
pwsmnd |
|- ( ( R e. Mnd /\ I e. V ) -> Y e. Mnd ) |
15 |
14
|
adantr |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> Y e. Mnd ) |
16 |
2 3
|
mulgnn0cl |
|- ( ( Y e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .xb X ) e. B ) |
17 |
15 10 11 16
|
syl3anc |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( N .xb X ) e. B ) |
18 |
|
fveq1 |
|- ( x = ( N .xb X ) -> ( x ` A ) = ( ( N .xb X ) ` A ) ) |
19 |
|
eqid |
|- ( x e. B |-> ( x ` A ) ) = ( x e. B |-> ( x ` A ) ) |
20 |
|
fvex |
|- ( ( N .xb X ) ` A ) e. _V |
21 |
18 19 20
|
fvmpt |
|- ( ( N .xb X ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( ( N .xb X ) ` A ) ) |
22 |
17 21
|
syl |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( ( N .xb X ) ` A ) ) |
23 |
|
fveq1 |
|- ( x = X -> ( x ` A ) = ( X ` A ) ) |
24 |
|
fvex |
|- ( X ` A ) e. _V |
25 |
23 19 24
|
fvmpt |
|- ( X e. B -> ( ( x e. B |-> ( x ` A ) ) ` X ) = ( X ` A ) ) |
26 |
11 25
|
syl |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( x e. B |-> ( x ` A ) ) ` X ) = ( X ` A ) ) |
27 |
26
|
oveq2d |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) = ( N .x. ( X ` A ) ) ) |
28 |
13 22 27
|
3eqtr3d |
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) ) |