Step |
Hyp |
Ref |
Expression |
1 |
|
mpfsubrg.q |
|- Q = ran ( ( I evalSub S ) ` R ) |
2 |
|
mpfaddcl.p |
|- .+ = ( +g ` S ) |
3 |
|
eqid |
|- ( S ^s ( ( Base ` S ) ^m I ) ) = ( S ^s ( ( Base ` S ) ^m I ) ) |
4 |
|
eqid |
|- ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) |
5 |
1
|
mpfrcl |
|- ( F e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) ) |
6 |
5
|
adantr |
|- ( ( F e. Q /\ G e. Q ) -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) ) |
7 |
6
|
simp2d |
|- ( ( F e. Q /\ G e. Q ) -> S e. CRing ) |
8 |
|
ovexd |
|- ( ( F e. Q /\ G e. Q ) -> ( ( Base ` S ) ^m I ) e. _V ) |
9 |
1
|
mpfsubrg |
|- ( ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
10 |
6 9
|
syl |
|- ( ( F e. Q /\ G e. Q ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
11 |
4
|
subrgss |
|- ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
12 |
10 11
|
syl |
|- ( ( F e. Q /\ G e. Q ) -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
13 |
|
simpl |
|- ( ( F e. Q /\ G e. Q ) -> F e. Q ) |
14 |
12 13
|
sseldd |
|- ( ( F e. Q /\ G e. Q ) -> F e. ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
15 |
|
simpr |
|- ( ( F e. Q /\ G e. Q ) -> G e. Q ) |
16 |
12 15
|
sseldd |
|- ( ( F e. Q /\ G e. Q ) -> G e. ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
17 |
|
eqid |
|- ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) |
18 |
3 4 7 8 14 16 2 17
|
pwsplusgval |
|- ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) = ( F oF .+ G ) ) |
19 |
17
|
subrgacl |
|- ( ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) /\ F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q ) |
20 |
19
|
3expib |
|- ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q ) ) |
21 |
10 20
|
mpcom |
|- ( ( F e. Q /\ G e. Q ) -> ( F ( +g ` ( S ^s ( ( Base ` S ) ^m I ) ) ) G ) e. Q ) |
22 |
18 21
|
eqeltrrd |
|- ( ( F e. Q /\ G e. Q ) -> ( F oF .+ G ) e. Q ) |