This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsplusgval

Description: Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbasmpt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsbasmpt.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
prdsplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
prdsplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
prdsplusgval.p ⊢ + = ( +g ‘ 𝑌 )
Assertion prdsplusgval ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +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 fnex ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
10 5 4 9 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
11 5 fndmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
12 1 3 10 2 11 8 prdsplusg ⊢ ( 𝜑 → + = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) ) )
13 fveq1 ⊢ ( 𝑦 = 𝐹 → ( 𝑦 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 fveq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
15 13 14 oveqan12d ⊢ ( ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) → ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
17 16 mpteq2dv ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
18 4 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
19 12 17 6 7 18 ovmpod ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )