Metamath Proof Explorer

Theorem coe1addfv

Description: A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 coe1add.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 coe1add.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 coe1add.p ⊢ ✚ = ( +g ‘ 𝑌 )
4 coe1add.q ⊢ + = ( +g ‘ 𝑅 )
5 1 2 3 4 coe1add ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) )
6 5 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) )
7 6 fveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) ‘ 𝑋 ) )
8 eqid ⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 8 2 1 9 coe1f ⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
11 10 ffnd ⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) Fn ℕ0 )
12 11 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐹 ) Fn ℕ0 )
13 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( coe1 ‘ 𝐹 ) Fn ℕ0 )
14 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
15 14 2 1 9 coe1f ⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
16 15 ffnd ⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) Fn ℕ0 )
17 16 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) Fn ℕ0 )
18 17 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( coe1 ‘ 𝐺 ) Fn ℕ0 )
19 nn0ex ⊢ ℕ0 ∈ V
20 19 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ℕ0 ∈ V )
21 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝑋 ∈ ℕ0 )
22 fnfvof ⊢ ( ( ( ( coe1 ‘ 𝐹 ) Fn ℕ0 ∧ ( coe1 ‘ 𝐺 ) Fn ℕ0 ) ∧ ( ℕ0 ∈ V ∧ 𝑋 ∈ ℕ0 ) ) → ( ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )
23 13 18 20 21 22 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )
24 7 23 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )