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

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 ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsplusgval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsplusgval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
pwsplusgval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
pwsplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
pwsplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
pwsplusgval.a ⊢ + = ( +g ‘ 𝑅 )
pwsplusgval.p ⊢ ✚ = ( +g ‘ 𝑌 )
Assertion pwsplusgval ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )

Proof

Step Hyp Ref Expression
1 pwsplusgval.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsplusgval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwsplusgval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 pwsplusgval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 pwsplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
6 pwsplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
7 pwsplusgval.a ⊢ + = ( +g ‘ 𝑅 )
8 pwsplusgval.p ⊢ ✚ = ( +g ‘ 𝑌 )
9 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
10 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
11 fvexd ⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
12 fnconstg ⊢ ( 𝑅 ∈ 𝑉 → ( 𝐼 × { 𝑅 } ) Fn 𝐼 )
13 3 12 syl ⊢ ( 𝜑 → ( 𝐼 × { 𝑅 } ) Fn 𝐼 )
14 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
15 1 14 pwsval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
16 3 4 15 syl2anc ⊢ ( 𝜑 → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
17 16 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
18 2 17 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
19 5 18 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
20 6 18 eleqtrd ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
21 eqid ⊢ ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
22 9 10 11 4 13 19 20 21 prdsplusgval ⊢ ( 𝜑 → ( 𝐹 ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
23 fvconst2g ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
24 3 23 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
25 24 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( +g ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( +g ‘ 𝑅 ) )
26 25 7 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( +g ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = + )
27 26 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
28 27 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
29 22 28 eqtrd ⊢ ( 𝜑 → ( 𝐹 ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
30 16 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
31 8 30 eqtrid ⊢ ( 𝜑 → ✚ = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
32 31 oveqd ⊢ ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) 𝐺 ) )
33 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
34 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ V )
35 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
36 1 35 2 3 4 5 pwselbas ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
37 36 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
38 1 35 2 3 4 6 pwselbas ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
39 38 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 ‘ 𝑥 ) ) )
40 4 33 34 37 39 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
41 29 32 40 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )