# Metamath Proof Explorer

## Theorem pwsplusgval

Description: Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsplusgval.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
pwsplusgval.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
pwsplusgval.r ${⊢}{\phi }\to {R}\in {V}$
pwsplusgval.i ${⊢}{\phi }\to {I}\in {W}$
pwsplusgval.f ${⊢}{\phi }\to {F}\in {B}$
pwsplusgval.g ${⊢}{\phi }\to {G}\in {B}$
pwsplusgval.a
pwsplusgval.p
Assertion pwsplusgval

### Proof

Step Hyp Ref Expression
1 pwsplusgval.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pwsplusgval.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 pwsplusgval.r ${⊢}{\phi }\to {R}\in {V}$
4 pwsplusgval.i ${⊢}{\phi }\to {I}\in {W}$
5 pwsplusgval.f ${⊢}{\phi }\to {F}\in {B}$
6 pwsplusgval.g ${⊢}{\phi }\to {G}\in {B}$
7 pwsplusgval.a
8 pwsplusgval.p
9 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
10 eqid ${⊢}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
11 fvexd ${⊢}{\phi }\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
12 fnconstg ${⊢}{R}\in {V}\to \left({I}×\left\{{R}\right\}\right)Fn{I}$
13 3 12 syl ${⊢}{\phi }\to \left({I}×\left\{{R}\right\}\right)Fn{I}$
14 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
15 1 14 pwsval ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {Y}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
16 3 4 15 syl2anc ${⊢}{\phi }\to {Y}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
17 16 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
18 2 17 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
19 5 18 eleqtrd ${⊢}{\phi }\to {F}\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
20 6 18 eleqtrd ${⊢}{\phi }\to {G}\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
21 eqid ${⊢}{+}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}={+}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
22 9 10 11 4 13 19 20 21 prdsplusgval ${⊢}{\phi }\to {F}{+}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}{G}=\left({x}\in {I}⟼{F}\left({x}\right){+}_{\left({I}×\left\{{R}\right\}\right)\left({x}\right)}{G}\left({x}\right)\right)$
23 fvconst2g ${⊢}\left({R}\in {V}\wedge {x}\in {I}\right)\to \left({I}×\left\{{R}\right\}\right)\left({x}\right)={R}$
24 3 23 sylan ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({I}×\left\{{R}\right\}\right)\left({x}\right)={R}$
25 24 fveq2d ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {+}_{\left({I}×\left\{{R}\right\}\right)\left({x}\right)}={+}_{{R}}$
26 25 7 syl6eqr
27 26 oveqd
28 27 mpteq2dva
29 22 28 eqtrd
30 16 fveq2d ${⊢}{\phi }\to {+}_{{Y}}={+}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
31 8 30 syl5eq
32 31 oveqd
33 fvexd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {F}\left({x}\right)\in \mathrm{V}$
34 fvexd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {G}\left({x}\right)\in \mathrm{V}$
35 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
36 1 35 2 3 4 5 pwselbas ${⊢}{\phi }\to {F}:{I}⟶{\mathrm{Base}}_{{R}}$
37 36 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {I}⟼{F}\left({x}\right)\right)$
38 1 35 2 3 4 6 pwselbas ${⊢}{\phi }\to {G}:{I}⟶{\mathrm{Base}}_{{R}}$
39 38 feqmptd ${⊢}{\phi }\to {G}=\left({x}\in {I}⟼{G}\left({x}\right)\right)$
40 4 33 34 37 39 offval2
41 29 32 40 3eqtr4d