Metamath Proof Explorer

Theorem coe1subfv

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

Ref Expression
Hypotheses coe1sub.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
coe1sub.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
coe1sub.p ⊢ − = ( -g ‘ 𝑌 )
coe1sub.q ⊢ 𝑁 = ( -g ‘ 𝑅 )
Assertion coe1subfv ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) 𝑁 ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 coe1sub.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 coe1sub.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 coe1sub.p ⊢ − = ( -g ‘ 𝑌 )
4 coe1sub.q ⊢ 𝑁 = ( -g ‘ 𝑅 )
5 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝑅 ∈ Ring )
6 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
7 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
8 6 7 syl ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Grp )
9 2 3 grpsubcl ⊢ ( ( 𝑌 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) ∈ 𝐵 )
10 8 9 syl3an1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) ∈ 𝐵 )
11 10 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( 𝐹 − 𝐺 ) ∈ 𝐵 )
12 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝐺 ∈ 𝐵 )
13 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝑋 ∈ ℕ0 )
14 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
15 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
16 1 2 14 15 coe1addfv ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 − 𝐺 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐹 − 𝐺 ) ( +g ‘ 𝑌 ) 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )
17 5 11 12 13 16 syl31anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐹 − 𝐺 ) ( +g ‘ 𝑌 ) 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )
18 8 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑌 ∈ Grp )
19 18 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝑌 ∈ Grp )
20 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝐹 ∈ 𝐵 )
21 2 14 3 grpnpcan ⊢ ( ( 𝑌 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 − 𝐺 ) ( +g ‘ 𝑌 ) 𝐺 ) = 𝐹 )
22 19 20 12 21 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐹 − 𝐺 ) ( +g ‘ 𝑌 ) 𝐺 ) = 𝐹 )
23 22 fveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( coe1 ‘ ( ( 𝐹 − 𝐺 ) ( +g ‘ 𝑌 ) 𝐺 ) ) = ( coe1 ‘ 𝐹 ) )
24 23 fveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐹 − 𝐺 ) ( +g ‘ 𝑌 ) 𝐺 ) ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) )
25 17 24 eqtr3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) )
26 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
27 26 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ Grp )
28 27 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → 𝑅 ∈ Grp )
29 eqid ⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
30 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
31 29 2 1 30 coe1f ⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
32 31 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
33 32 ffvelrnda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
34 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
35 34 2 1 30 coe1f ⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
36 35 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
37 36 ffvelrnda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
38 eqid ⊢ ( coe1 ‘ ( 𝐹 − 𝐺 ) ) = ( coe1 ‘ ( 𝐹 − 𝐺 ) )
39 38 2 1 30 coe1f ⊢ ( ( 𝐹 − 𝐺 ) ∈ 𝐵 → ( coe1 ‘ ( 𝐹 − 𝐺 ) ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
40 10 39 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 − 𝐺 ) ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
41 40 ffvelrnda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
42 30 15 4 grpsubadd ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) 𝑁 ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ↔ ( ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) ) )
43 28 33 37 41 42 syl13anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) 𝑁 ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ↔ ( ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) ) )
44 25 43 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) 𝑁 ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) )
45 44 eqcomd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) 𝑁 ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) ) )