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

Metamath Proof Explorer

Theorem coe1add

Description: The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015)

Ref Expression
Hypotheses coe1add.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
coe1add.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
coe1add.p ⊢ ✚ = ( +g ‘ 𝑌 )
coe1add.q ⊢ + = ( +g ‘ 𝑅 )
Assertion coe1add ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 coe1add.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 coe1add.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 coe1add.p ⊢ ✚ = ( +g ‘ 𝑌 )
4 coe1add.q ⊢ + = ( +g ‘ 𝑅 )
5 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6 1 2 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
7 1 5 3 ply1plusg ⊢ ✚ = ( +g ‘ ( 1o mPoly 𝑅 ) )
8 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
9 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
10 5 6 4 7 8 9 mpladd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )
11 10 coeq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( ( 𝐹 ∘f + 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 1 2 12 ply1basf ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) )
14 13 ffnd ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 Fn ( ℕ0 ↑m 1o ) )
15 14 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 Fn ( ℕ0 ↑m 1o ) )
16 1 2 12 ply1basf ⊢ ( 𝐺 ∈ 𝐵 → 𝐺 : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) )
17 16 ffnd ⊢ ( 𝐺 ∈ 𝐵 → 𝐺 Fn ( ℕ0 ↑m 1o ) )
18 17 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 Fn ( ℕ0 ↑m 1o ) )
19 df1o2 ⊢ 1o = { ∅ }
20 nn0ex ⊢ ℕ0 ∈ V
21 0ex ⊢ ∅ ∈ V
22 eqid ⊢ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) )
23 19 20 21 22 mapsnf1o3 ⊢ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o )
24 f1of ⊢ ( ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) → ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o ) )
25 23 24 mp1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o ) )
26 ovexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ℕ0 ↑m 1o ) ∈ V )
27 20 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ℕ0 ∈ V )
28 inidm ⊢ ( ( ℕ0 ↑m 1o ) ∩ ( ℕ0 ↑m 1o ) ) = ( ℕ0 ↑m 1o )
29 15 18 25 26 26 27 28 ofco ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ∘f + 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ∘f + ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) )
30 11 29 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ∘f + ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) )
31 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
32 2 3 ringacl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ✚ 𝐺 ) ∈ 𝐵 )
33 31 32 syl3an1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ✚ 𝐺 ) ∈ 𝐵 )
34 eqid ⊢ ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) )
35 34 2 1 22 coe1fval2 ⊢ ( ( 𝐹 ✚ 𝐺 ) ∈ 𝐵 → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
36 33 35 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
37 eqid ⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
38 37 2 1 22 coe1fval2 ⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) = ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
39 38 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐹 ) = ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
40 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
41 40 2 1 22 coe1fval2 ⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) = ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
42 41 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) = ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
43 39 42 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) = ( ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ∘f + ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) )
44 30 36 43 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) )