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

Metamath Proof Explorer

Theorem frlmplusgval

Description: Addition in a free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses frlmplusgval.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmplusgval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
frlmplusgval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
frlmplusgval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
frlmplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
frlmplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
frlmplusgval.a ⊢ + = ( +g ‘ 𝑅 )
frlmplusgval.p ⊢ ✚ = ( +g ‘ 𝑌 )
Assertion frlmplusgval ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )

Proof

Step Hyp Ref Expression
1 frlmplusgval.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmplusgval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 frlmplusgval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 frlmplusgval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 frlmplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
6 frlmplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
7 frlmplusgval.a ⊢ + = ( +g ‘ 𝑅 )
8 frlmplusgval.p ⊢ ✚ = ( +g ‘ 𝑌 )
9 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
10 1 9 frlmpws ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) ) )
11 3 4 10 syl2anc ⊢ ( 𝜑 → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) ) )
12 11 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) ) ) )
13 fvex ⊢ ( Base ‘ 𝑌 ) ∈ V
14 eqid ⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) )
15 eqid ⊢ ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
16 14 15 ressplusg ⊢ ( ( Base ‘ 𝑌 ) ∈ V → ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( +g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) ) ) )
17 13 16 ax-mp ⊢ ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( +g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝑌 ) ) )
18 12 8 17 3eqtr4g ⊢ ( 𝜑 → ✚ = ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
19 18 oveqd ⊢ ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝐺 ) )
20 eqid ⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
21 eqid ⊢ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
22 fvexd ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ V )
23 1 2 frlmpws ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
24 3 4 23 syl2anc ⊢ ( 𝜑 → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
25 24 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
26 2 25 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
27 eqid ⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 )
28 27 21 ressbasss ⊢ ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
29 26 28 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
30 29 5 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
31 29 6 sseldd ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
32 rlmplusg ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
33 7 32 eqtri ⊢ + = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
34 20 21 22 4 30 31 33 15 pwsplusgval ⊢ ( 𝜑 → ( 𝐹 ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )
35 19 34 eqtrd ⊢ ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )