Proof of Theorem ply1rem
Step | Hyp | Ref
| Expression |
1 | | ply1rem.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ NzRing) |
2 | | nzrring 19082 |
. . . . . . . . 9
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | ply1rem.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
5 | | ply1rem.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Poly1‘𝑅) |
6 | | ply1rem.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑃) |
7 | | ply1rem.k |
. . . . . . . . . . 11
⊢ 𝐾 = (Base‘𝑅) |
8 | | ply1rem.x |
. . . . . . . . . . 11
⊢ 𝑋 = (var1‘𝑅) |
9 | | ply1rem.m |
. . . . . . . . . . 11
⊢ − =
(-g‘𝑃) |
10 | | ply1rem.a |
. . . . . . . . . . 11
⊢ 𝐴 = (algSc‘𝑃) |
11 | | ply1rem.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) |
12 | | ply1rem.o |
. . . . . . . . . . 11
⊢ 𝑂 = (eval1‘𝑅) |
13 | | ply1rem.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ CRing) |
14 | | ply1rem.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ 𝐾) |
15 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
16 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (
deg1 ‘𝑅) =
( deg1 ‘𝑅) |
17 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
18 | 5, 6, 7, 8, 9, 10,
11, 12, 1, 13, 14, 15, 16, 17 | ply1remlem 23726 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ∈ (Monic1p‘𝑅) ∧ (( deg1
‘𝑅)‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ {(0g‘𝑅)}) = {𝑁})) |
19 | 18 | simp1d 1066 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅)) |
20 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
21 | 20, 15 | mon1puc1p 23714 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈
(Monic1p‘𝑅)) → 𝐺 ∈ (Unic1p‘𝑅)) |
22 | 3, 19, 21 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (Unic1p‘𝑅)) |
23 | | ply1rem.e |
. . . . . . . . 9
⊢ 𝐸 = (rem1p‘𝑅) |
24 | 23, 5, 6, 20, 16 | r1pdeglt 23722 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) < (( deg1 ‘𝑅)‘𝐺)) |
25 | 3, 4, 22, 24 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) < (( deg1 ‘𝑅)‘𝐺)) |
26 | 18 | simp2d 1067 |
. . . . . . 7
⊢ (𝜑 → (( deg1
‘𝑅)‘𝐺) = 1) |
27 | 25, 26 | breqtrd 4609 |
. . . . . 6
⊢ (𝜑 → (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) < 1) |
28 | | 1e0p1 11428 |
. . . . . 6
⊢ 1 = (0 +
1) |
29 | 27, 28 | syl6breq 4624 |
. . . . 5
⊢ (𝜑 → (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) < (0 + 1)) |
30 | | 0nn0 11184 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
31 | | nn0leltp1 11313 |
. . . . . 6
⊢ ((((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 ∧ 0 ∈
ℕ0) → ((( deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) < (0 + 1))) |
32 | 30, 31 | mpan2 703 |
. . . . 5
⊢ (((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 → (((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) < (0 + 1))) |
33 | 29, 32 | syl5ibrcom 236 |
. . . 4
⊢ (𝜑 → ((( deg1
‘𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 → ((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0)) |
34 | | elsni 4142 |
. . . . . 6
⊢ (((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞} → ((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) = -∞) |
35 | | 0xr 9965 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
36 | | mnfle 11845 |
. . . . . . 7
⊢ (0 ∈
ℝ* → -∞ ≤ 0) |
37 | 35, 36 | ax-mp 5 |
. . . . . 6
⊢ -∞
≤ 0 |
38 | 34, 37 | syl6eqbr 4622 |
. . . . 5
⊢ (((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞} → ((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0) |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝜑 → ((( deg1
‘𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞} → ((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0)) |
40 | 23, 5, 6, 20 | r1pcl 23721 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹𝐸𝐺) ∈ 𝐵) |
41 | 3, 4, 22, 40 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝐹𝐸𝐺) ∈ 𝐵) |
42 | 16, 5, 6 | deg1cl 23647 |
. . . . . 6
⊢ ((𝐹𝐸𝐺) ∈ 𝐵 → (( deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪
{-∞})) |
43 | 41, 42 | syl 17 |
. . . . 5
⊢ (𝜑 → (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪
{-∞})) |
44 | | elun 3715 |
. . . . 5
⊢ (((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪
{-∞}) ↔ ((( deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ ((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞})) |
45 | 43, 44 | sylib 207 |
. . . 4
⊢ (𝜑 → ((( deg1
‘𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ ((
deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞})) |
46 | 33, 39, 45 | mpjaod 395 |
. . 3
⊢ (𝜑 → (( deg1
‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0) |
47 | 16, 5, 6, 10 | deg1le0 23675 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝐹𝐸𝐺) ∈ 𝐵) → ((( deg1 ‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (𝐹𝐸𝐺) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0)))) |
48 | 3, 41, 47 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((( deg1
‘𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (𝐹𝐸𝐺) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0)))) |
49 | 46, 48 | mpbid 221 |
. 2
⊢ (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))) |
50 | | eqid 2610 |
. . . . . . . . 9
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
51 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑃) = (.r‘𝑃) |
52 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝑃) = (+g‘𝑃) |
53 | 5, 6, 20, 50, 23, 51, 52 | r1pid 23723 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → 𝐹 = (((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺))) |
54 | 3, 4, 22, 53 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺))) |
55 | 54 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝑂‘𝐹) = (𝑂‘(((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺)))) |
56 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
57 | 12, 5, 56, 7 | evl1rhm 19517 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
58 | 13, 57 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
59 | | rhmghm 18548 |
. . . . . . . 8
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂 ∈ (𝑃 GrpHom (𝑅 ↑s 𝐾))) |
60 | 58, 59 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ (𝑃 GrpHom (𝑅 ↑s 𝐾))) |
61 | 5 | ply1ring 19439 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
62 | 3, 61 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ Ring) |
63 | 50, 5, 6, 20 | q1pcl 23719 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
64 | 3, 4, 22, 63 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
65 | 5, 6, 15 | mon1pcl 23708 |
. . . . . . . . 9
⊢ (𝐺 ∈
(Monic1p‘𝑅) → 𝐺 ∈ 𝐵) |
66 | 19, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
67 | 6, 51 | ringcl 18384 |
. . . . . . . 8
⊢ ((𝑃 ∈ Ring ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ∈ 𝐵) |
68 | 62, 64, 66, 67 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ∈ 𝐵) |
69 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘(𝑅 ↑s 𝐾)) = (+g‘(𝑅 ↑s 𝐾)) |
70 | 6, 52, 69 | ghmlin 17488 |
. . . . . . 7
⊢ ((𝑂 ∈ (𝑃 GrpHom (𝑅 ↑s 𝐾)) ∧ ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ∈ 𝐵 ∧ (𝐹𝐸𝐺) ∈ 𝐵) → (𝑂‘(((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺))) = ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))(+g‘(𝑅 ↑s 𝐾))(𝑂‘(𝐹𝐸𝐺)))) |
71 | 60, 68, 41, 70 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺))) = ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))(+g‘(𝑅 ↑s 𝐾))(𝑂‘(𝐹𝐸𝐺)))) |
72 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
73 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑅)
∈ V |
74 | 7, 73 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐾 ∈ V |
75 | 74 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ V) |
76 | 6, 72 | rhmf 18549 |
. . . . . . . . 9
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
77 | 58, 76 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
78 | 77, 68 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
79 | 77, 41 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝐹𝐸𝐺)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
80 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
81 | 56, 72, 1, 75, 78, 79, 80, 69 | pwsplusgval 15973 |
. . . . . 6
⊢ (𝜑 → ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))(+g‘(𝑅 ↑s 𝐾))(𝑂‘(𝐹𝐸𝐺))) = ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∘𝑓
(+g‘𝑅)(𝑂‘(𝐹𝐸𝐺)))) |
82 | 55, 71, 81 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (𝑂‘𝐹) = ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∘𝑓
(+g‘𝑅)(𝑂‘(𝐹𝐸𝐺)))) |
83 | 82 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑁) = (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∘𝑓
(+g‘𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁)) |
84 | 56, 7, 72, 1, 75, 78 | pwselbas 15972 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)):𝐾⟶𝐾) |
85 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)):𝐾⟶𝐾 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) Fn 𝐾) |
86 | 84, 85 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) Fn 𝐾) |
87 | 56, 7, 72, 1, 75, 79 | pwselbas 15972 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝐹𝐸𝐺)):𝐾⟶𝐾) |
88 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑂‘(𝐹𝐸𝐺)):𝐾⟶𝐾 → (𝑂‘(𝐹𝐸𝐺)) Fn 𝐾) |
89 | 87, 88 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐹𝐸𝐺)) Fn 𝐾) |
90 | | fnfvof 6809 |
. . . . . 6
⊢ ((((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) Fn 𝐾 ∧ (𝑂‘(𝐹𝐸𝐺)) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑁 ∈ 𝐾)) → (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∘𝑓
(+g‘𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁) = (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))‘𝑁)(+g‘𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁))) |
91 | 86, 89, 75, 14, 90 | syl22anc 1319 |
. . . . 5
⊢ (𝜑 → (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∘𝑓
(+g‘𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁) = (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))‘𝑁)(+g‘𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁))) |
92 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘(𝑅 ↑s 𝐾)) = (.r‘(𝑅 ↑s 𝐾)) |
93 | 6, 51, 92 | rhmmul 18550 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺))) |
94 | 58, 64, 66, 93 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺))) |
95 | 77, 64 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
96 | 77, 66 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑂‘𝐺) ∈ (Base‘(𝑅 ↑s 𝐾))) |
97 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
98 | 56, 72, 1, 75, 95, 96, 97, 92 | pwsmulrval 15974 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))) |
99 | 94, 98 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))) |
100 | 99 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))‘𝑁) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑁)) |
101 | 56, 7, 72, 1, 75, 95 | pwselbas 15972 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)):𝐾⟶𝐾) |
102 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)):𝐾⟶𝐾 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾) |
103 | 101, 102 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾) |
104 | 56, 7, 72, 1, 75, 96 | pwselbas 15972 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘𝐺):𝐾⟶𝐾) |
105 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑂‘𝐺):𝐾⟶𝐾 → (𝑂‘𝐺) Fn 𝐾) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝐺) Fn 𝐾) |
107 | | fnfvof 6809 |
. . . . . . . 8
⊢ ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾 ∧ (𝑂‘𝐺) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑁 ∈ 𝐾)) → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑁) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)((𝑂‘𝐺)‘𝑁))) |
108 | 103, 106,
75, 14, 107 | syl22anc 1319 |
. . . . . . 7
⊢ (𝜑 → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑁) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)((𝑂‘𝐺)‘𝑁))) |
109 | | snidg 4153 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ 𝐾 → 𝑁 ∈ {𝑁}) |
110 | 14, 109 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ {𝑁}) |
111 | 18 | simp3d 1068 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡(𝑂‘𝐺) “ {(0g‘𝑅)}) = {𝑁}) |
112 | 110, 111 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (◡(𝑂‘𝐺) “ {(0g‘𝑅)})) |
113 | | fniniseg 6246 |
. . . . . . . . . . . 12
⊢ ((𝑂‘𝐺) Fn 𝐾 → (𝑁 ∈ (◡(𝑂‘𝐺) “ {(0g‘𝑅)}) ↔ (𝑁 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑁) = (0g‘𝑅)))) |
114 | 106, 113 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ (◡(𝑂‘𝐺) “ {(0g‘𝑅)}) ↔ (𝑁 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑁) = (0g‘𝑅)))) |
115 | 112, 114 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑁) = (0g‘𝑅))) |
116 | 115 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘𝐺)‘𝑁) = (0g‘𝑅)) |
117 | 116 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)((𝑂‘𝐺)‘𝑁)) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)(0g‘𝑅))) |
118 | 101, 14 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁) ∈ 𝐾) |
119 | 7, 97, 17 | ringrz 18411 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁) ∈ 𝐾) → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
120 | 3, 118, 119 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
121 | 117, 120 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑁)(.r‘𝑅)((𝑂‘𝐺)‘𝑁)) = (0g‘𝑅)) |
122 | 100, 108,
121 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → ((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))‘𝑁) = (0g‘𝑅)) |
123 | 122 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))‘𝑁)(+g‘𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)) = ((0g‘𝑅)(+g‘𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁))) |
124 | | ringgrp 18375 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
125 | 3, 124 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
126 | 87, 14 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → ((𝑂‘(𝐹𝐸𝐺))‘𝑁) ∈ 𝐾) |
127 | 7, 80, 17 | grplid 17275 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ ((𝑂‘(𝐹𝐸𝐺))‘𝑁) ∈ 𝐾) → ((0g‘𝑅)(+g‘𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)) = ((𝑂‘(𝐹𝐸𝐺))‘𝑁)) |
128 | 125, 126,
127 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑅)(+g‘𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)) = ((𝑂‘(𝐹𝐸𝐺))‘𝑁)) |
129 | 91, 123, 128 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (((𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) ∘𝑓
(+g‘𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁) = ((𝑂‘(𝐹𝐸𝐺))‘𝑁)) |
130 | 49 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝐹𝐸𝐺)) = (𝑂‘(𝐴‘((coe1‘(𝐹𝐸𝐺))‘0)))) |
131 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(coe1‘(𝐹𝐸𝐺)) = (coe1‘(𝐹𝐸𝐺)) |
132 | 131, 6, 5, 7 | coe1f 19402 |
. . . . . . . . . 10
⊢ ((𝐹𝐸𝐺) ∈ 𝐵 → (coe1‘(𝐹𝐸𝐺)):ℕ0⟶𝐾) |
133 | 41, 132 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(coe1‘(𝐹𝐸𝐺)):ℕ0⟶𝐾) |
134 | | ffvelrn 6265 |
. . . . . . . . 9
⊢
(((coe1‘(𝐹𝐸𝐺)):ℕ0⟶𝐾 ∧ 0 ∈
ℕ0) → ((coe1‘(𝐹𝐸𝐺))‘0) ∈ 𝐾) |
135 | 133, 30, 134 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 →
((coe1‘(𝐹𝐸𝐺))‘0) ∈ 𝐾) |
136 | 12, 5, 7, 10 | evl1sca 19519 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧
((coe1‘(𝐹𝐸𝐺))‘0) ∈ 𝐾) → (𝑂‘(𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))) = (𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})) |
137 | 13, 135, 136 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))) = (𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})) |
138 | 130, 137 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐹𝐸𝐺)) = (𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})) |
139 | 138 | fveq1d 6105 |
. . . . 5
⊢ (𝜑 → ((𝑂‘(𝐹𝐸𝐺))‘𝑁) = ((𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})‘𝑁)) |
140 | | fvex 6113 |
. . . . . . 7
⊢
((coe1‘(𝐹𝐸𝐺))‘0) ∈ V |
141 | 140 | fvconst2 6374 |
. . . . . 6
⊢ (𝑁 ∈ 𝐾 → ((𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0)) |
142 | 14, 141 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0)) |
143 | 139, 142 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝑂‘(𝐹𝐸𝐺))‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0)) |
144 | 83, 129, 143 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0)) |
145 | 144 | fveq2d 6107 |
. 2
⊢ (𝜑 → (𝐴‘((𝑂‘𝐹)‘𝑁)) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))) |
146 | 49, 145 | eqtr4d 2647 |
1
⊢ (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((𝑂‘𝐹)‘𝑁))) |