Metamath Proof Explorer


Theorem prdsplusgfval

Description: Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsbasmpt.y 𝑌 = ( 𝑆 Xs 𝑅 )
prdsbasmpt.b 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt.s ( 𝜑𝑆𝑉 )
prdsbasmpt.i ( 𝜑𝐼𝑊 )
prdsbasmpt.r ( 𝜑𝑅 Fn 𝐼 )
prdsplusgval.f ( 𝜑𝐹𝐵 )
prdsplusgval.g ( 𝜑𝐺𝐵 )
prdsplusgval.p + = ( +g𝑌 )
prdsplusgfval.j ( 𝜑𝐽𝐼 )
Assertion prdsplusgfval ( 𝜑 → ( ( 𝐹 + 𝐺 ) ‘ 𝐽 ) = ( ( 𝐹𝐽 ) ( +g ‘ ( 𝑅𝐽 ) ) ( 𝐺𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsbasmpt.b 𝐵 = ( Base ‘ 𝑌 )
3 prdsbasmpt.s ( 𝜑𝑆𝑉 )
4 prdsbasmpt.i ( 𝜑𝐼𝑊 )
5 prdsbasmpt.r ( 𝜑𝑅 Fn 𝐼 )
6 prdsplusgval.f ( 𝜑𝐹𝐵 )
7 prdsplusgval.g ( 𝜑𝐺𝐵 )
8 prdsplusgval.p + = ( +g𝑌 )
9 prdsplusgfval.j ( 𝜑𝐽𝐼 )
10 1 2 3 4 5 6 7 8 prdsplusgval ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) )
11 10 fveq1d ( 𝜑 → ( ( 𝐹 + 𝐺 ) ‘ 𝐽 ) = ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ‘ 𝐽 ) )
12 2fveq3 ( 𝑥 = 𝐽 → ( +g ‘ ( 𝑅𝑥 ) ) = ( +g ‘ ( 𝑅𝐽 ) ) )
13 fveq2 ( 𝑥 = 𝐽 → ( 𝐹𝑥 ) = ( 𝐹𝐽 ) )
14 fveq2 ( 𝑥 = 𝐽 → ( 𝐺𝑥 ) = ( 𝐺𝐽 ) )
15 12 13 14 oveq123d ( 𝑥 = 𝐽 → ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) = ( ( 𝐹𝐽 ) ( +g ‘ ( 𝑅𝐽 ) ) ( 𝐺𝐽 ) ) )
16 eqid ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) = ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) )
17 ovex ( ( 𝐹𝐽 ) ( +g ‘ ( 𝑅𝐽 ) ) ( 𝐺𝐽 ) ) ∈ V
18 15 16 17 fvmpt ( 𝐽𝐼 → ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ‘ 𝐽 ) = ( ( 𝐹𝐽 ) ( +g ‘ ( 𝑅𝐽 ) ) ( 𝐺𝐽 ) ) )
19 9 18 syl ( 𝜑 → ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ‘ 𝐽 ) = ( ( 𝐹𝐽 ) ( +g ‘ ( 𝑅𝐽 ) ) ( 𝐺𝐽 ) ) )
20 11 19 eqtrd ( 𝜑 → ( ( 𝐹 + 𝐺 ) ‘ 𝐽 ) = ( ( 𝐹𝐽 ) ( +g ‘ ( 𝑅𝐽 ) ) ( 𝐺𝐽 ) ) )