Proof of Theorem coe1subfv
Step | Hyp | Ref
| Expression |
1 | | simpl1 1193 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → 𝑅 ∈ Ring) |
2 | | coe1sub.y |
. . . . . . . . 9
⊢ 𝑌 = (Poly1‘𝑅) |
3 | 2 | ply1ring 21169 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑌 ∈ Ring) |
4 | | ringgrp 19567 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑌 ∈ Grp) |
6 | | coe1sub.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
7 | | coe1sub.p |
. . . . . . . 8
⊢ − =
(-g‘𝑌) |
8 | 6, 7 | grpsubcl 18443 |
. . . . . . 7
⊢ ((𝑌 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 − 𝐺) ∈ 𝐵) |
9 | 5, 8 | syl3an1 1165 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 − 𝐺) ∈ 𝐵) |
10 | 9 | adantr 484 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → (𝐹 − 𝐺) ∈ 𝐵) |
11 | | simpl3 1195 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → 𝐺 ∈ 𝐵) |
12 | | simpr 488 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → 𝑋 ∈
ℕ0) |
13 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑌) = (+g‘𝑌) |
14 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑅) = (+g‘𝑅) |
15 | 2, 6, 13, 14 | coe1addfv 21186 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ (𝐹 − 𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘((𝐹
−
𝐺)(+g‘𝑌)𝐺))‘𝑋) = (((coe1‘(𝐹 − 𝐺))‘𝑋)(+g‘𝑅)((coe1‘𝐺)‘𝑋))) |
16 | 1, 10, 11, 12, 15 | syl31anc 1375 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘((𝐹
−
𝐺)(+g‘𝑌)𝐺))‘𝑋) = (((coe1‘(𝐹 − 𝐺))‘𝑋)(+g‘𝑅)((coe1‘𝐺)‘𝑋))) |
17 | 5 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑌 ∈ Grp) |
18 | 17 | adantr 484 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → 𝑌 ∈ Grp) |
19 | | simpl2 1194 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → 𝐹 ∈ 𝐵) |
20 | 6, 13, 7 | grpnpcan 18455 |
. . . . . . 7
⊢ ((𝑌 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐹 − 𝐺)(+g‘𝑌)𝐺) = 𝐹) |
21 | 18, 19, 11, 20 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → ((𝐹 − 𝐺)(+g‘𝑌)𝐺) = 𝐹) |
22 | 21 | fveq2d 6721 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
(coe1‘((𝐹
−
𝐺)(+g‘𝑌)𝐺)) = (coe1‘𝐹)) |
23 | 22 | fveq1d 6719 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘((𝐹
−
𝐺)(+g‘𝑌)𝐺))‘𝑋) = ((coe1‘𝐹)‘𝑋)) |
24 | 16, 23 | eqtr3d 2779 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
(((coe1‘(𝐹
−
𝐺))‘𝑋)(+g‘𝑅)((coe1‘𝐺)‘𝑋)) = ((coe1‘𝐹)‘𝑋)) |
25 | | ringgrp 19567 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
26 | 25 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ Grp) |
27 | 26 | adantr 484 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → 𝑅 ∈ Grp) |
28 | | eqid 2737 |
. . . . . . 7
⊢
(coe1‘𝐹) = (coe1‘𝐹) |
29 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
30 | 28, 6, 2, 29 | coe1f 21132 |
. . . . . 6
⊢ (𝐹 ∈ 𝐵 → (coe1‘𝐹):ℕ0⟶(Base‘𝑅)) |
31 | 30 | 3ad2ant2 1136 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘𝐹):ℕ0⟶(Base‘𝑅)) |
32 | 31 | ffvelrnda 6904 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘𝐹)‘𝑋) ∈ (Base‘𝑅)) |
33 | | eqid 2737 |
. . . . . . 7
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
34 | 33, 6, 2, 29 | coe1f 21132 |
. . . . . 6
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶(Base‘𝑅)) |
35 | 34 | 3ad2ant3 1137 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘𝐺):ℕ0⟶(Base‘𝑅)) |
36 | 35 | ffvelrnda 6904 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘𝐺)‘𝑋) ∈ (Base‘𝑅)) |
37 | | eqid 2737 |
. . . . . . 7
⊢
(coe1‘(𝐹 − 𝐺)) = (coe1‘(𝐹 − 𝐺)) |
38 | 37, 6, 2, 29 | coe1f 21132 |
. . . . . 6
⊢ ((𝐹 − 𝐺) ∈ 𝐵 → (coe1‘(𝐹 − 𝐺)):ℕ0⟶(Base‘𝑅)) |
39 | 9, 38 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 − 𝐺)):ℕ0⟶(Base‘𝑅)) |
40 | 39 | ffvelrnda 6904 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘(𝐹
−
𝐺))‘𝑋) ∈ (Base‘𝑅)) |
41 | | coe1sub.q |
. . . . 5
⊢ 𝑁 = (-g‘𝑅) |
42 | 29, 14, 41 | grpsubadd 18451 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧
(((coe1‘𝐹)‘𝑋) ∈ (Base‘𝑅) ∧ ((coe1‘𝐺)‘𝑋) ∈ (Base‘𝑅) ∧ ((coe1‘(𝐹 − 𝐺))‘𝑋) ∈ (Base‘𝑅))) → ((((coe1‘𝐹)‘𝑋)𝑁((coe1‘𝐺)‘𝑋)) = ((coe1‘(𝐹 − 𝐺))‘𝑋) ↔ (((coe1‘(𝐹 − 𝐺))‘𝑋)(+g‘𝑅)((coe1‘𝐺)‘𝑋)) = ((coe1‘𝐹)‘𝑋))) |
43 | 27, 32, 36, 40, 42 | syl13anc 1374 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((((coe1‘𝐹)‘𝑋)𝑁((coe1‘𝐺)‘𝑋)) = ((coe1‘(𝐹 − 𝐺))‘𝑋) ↔ (((coe1‘(𝐹 − 𝐺))‘𝑋)(+g‘𝑅)((coe1‘𝐺)‘𝑋)) = ((coe1‘𝐹)‘𝑋))) |
44 | 24, 43 | mpbird 260 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
(((coe1‘𝐹)‘𝑋)𝑁((coe1‘𝐺)‘𝑋)) = ((coe1‘(𝐹 − 𝐺))‘𝑋)) |
45 | 44 | eqcomd 2743 |
1
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) →
((coe1‘(𝐹
−
𝐺))‘𝑋) = (((coe1‘𝐹)‘𝑋)𝑁((coe1‘𝐺)‘𝑋))) |