| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ply1rem.g | . . . 4
⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) | 
| 2 |  | ply1rem.1 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ NzRing) | 
| 3 |  | nzrring 20517 | . . . . . . . 8
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) | 
| 4 | 2, 3 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 5 |  | ply1rem.p | . . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) | 
| 6 | 5 | ply1ring 22250 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 7 | 4, 6 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 8 |  | ringgrp 20236 | . . . . . 6
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) | 
| 9 | 7, 8 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 10 |  | ply1rem.x | . . . . . . 7
⊢ 𝑋 = (var1‘𝑅) | 
| 11 |  | ply1rem.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑃) | 
| 12 | 10, 5, 11 | vr1cl 22220 | . . . . . 6
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) | 
| 13 | 4, 12 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 14 |  | ply1rem.a | . . . . . . . 8
⊢ 𝐴 = (algSc‘𝑃) | 
| 15 |  | ply1rem.k | . . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) | 
| 16 | 5, 14, 15, 11 | ply1sclf 22289 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) | 
| 17 | 4, 16 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐴:𝐾⟶𝐵) | 
| 18 |  | ply1rem.3 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ 𝐾) | 
| 19 | 17, 18 | ffvelcdmd 7104 | . . . . 5
⊢ (𝜑 → (𝐴‘𝑁) ∈ 𝐵) | 
| 20 |  | ply1rem.m | . . . . . 6
⊢  − =
(-g‘𝑃) | 
| 21 | 11, 20 | grpsubcl 19039 | . . . . 5
⊢ ((𝑃 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐴‘𝑁) ∈ 𝐵) → (𝑋 − (𝐴‘𝑁)) ∈ 𝐵) | 
| 22 | 9, 13, 19, 21 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝑋 − (𝐴‘𝑁)) ∈ 𝐵) | 
| 23 | 1, 22 | eqeltrid 2844 | . . 3
⊢ (𝜑 → 𝐺 ∈ 𝐵) | 
| 24 | 1 | fveq2i 6908 | . . . . . . 7
⊢ (𝐷‘𝐺) = (𝐷‘(𝑋 − (𝐴‘𝑁))) | 
| 25 |  | ply1rem.d | . . . . . . . 8
⊢ 𝐷 = (deg1‘𝑅) | 
| 26 | 25, 5, 11 | deg1xrcl 26122 | . . . . . . . . . . 11
⊢ ((𝐴‘𝑁) ∈ 𝐵 → (𝐷‘(𝐴‘𝑁)) ∈
ℝ*) | 
| 27 | 19, 26 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐷‘(𝐴‘𝑁)) ∈
ℝ*) | 
| 28 |  | 0xr 11309 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ* | 
| 29 | 28 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ*) | 
| 30 |  | 1re 11262 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 31 |  | rexr 11308 | . . . . . . . . . . 11
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) | 
| 32 | 30, 31 | mp1i 13 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ*) | 
| 33 | 25, 5, 15, 14 | deg1sclle 26152 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ 𝐾) → (𝐷‘(𝐴‘𝑁)) ≤ 0) | 
| 34 | 4, 18, 33 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝐷‘(𝐴‘𝑁)) ≤ 0) | 
| 35 |  | 0lt1 11786 | . . . . . . . . . . 11
⊢ 0 <
1 | 
| 36 | 35 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 0 < 1) | 
| 37 | 27, 29, 32, 34, 36 | xrlelttrd 13203 | . . . . . . . . 9
⊢ (𝜑 → (𝐷‘(𝐴‘𝑁)) < 1) | 
| 38 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) | 
| 39 | 38, 11 | mgpbas 20143 | . . . . . . . . . . . . 13
⊢ 𝐵 =
(Base‘(mulGrp‘𝑃)) | 
| 40 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) | 
| 41 | 39, 40 | mulg1 19100 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 →
(1(.g‘(mulGrp‘𝑃))𝑋) = 𝑋) | 
| 42 | 13, 41 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(1(.g‘(mulGrp‘𝑃))𝑋) = 𝑋) | 
| 43 | 42 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 → (𝐷‘(1(.g‘(mulGrp‘𝑃))𝑋)) = (𝐷‘𝑋)) | 
| 44 |  | 1nn0 12544 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ0 | 
| 45 | 25, 5, 10, 38, 40 | deg1pw 26161 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ NzRing ∧ 1 ∈
ℕ0) → (𝐷‘(1(.g‘(mulGrp‘𝑃))𝑋)) = 1) | 
| 46 | 2, 44, 45 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → (𝐷‘(1(.g‘(mulGrp‘𝑃))𝑋)) = 1) | 
| 47 | 43, 46 | eqtr3d 2778 | . . . . . . . . 9
⊢ (𝜑 → (𝐷‘𝑋) = 1) | 
| 48 | 37, 47 | breqtrrd 5170 | . . . . . . . 8
⊢ (𝜑 → (𝐷‘(𝐴‘𝑁)) < (𝐷‘𝑋)) | 
| 49 | 5, 25, 4, 11, 20, 13, 19, 48 | deg1sub 26148 | . . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑋 − (𝐴‘𝑁))) = (𝐷‘𝑋)) | 
| 50 | 24, 49 | eqtrid 2788 | . . . . . 6
⊢ (𝜑 → (𝐷‘𝐺) = (𝐷‘𝑋)) | 
| 51 | 50, 47 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (𝐷‘𝐺) = 1) | 
| 52 | 51, 44 | eqeltrdi 2848 | . . . 4
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℕ0) | 
| 53 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 54 | 25, 5, 53, 11 | deg1nn0clb 26130 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐺 ≠ (0g‘𝑃) ↔ (𝐷‘𝐺) ∈
ℕ0)) | 
| 55 | 4, 23, 54 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐺 ≠ (0g‘𝑃) ↔ (𝐷‘𝐺) ∈
ℕ0)) | 
| 56 | 52, 55 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃)) | 
| 57 | 51 | fveq2d 6909 | . . . 4
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) = ((coe1‘𝐺)‘1)) | 
| 58 | 1 | fveq2i 6908 | . . . . . 6
⊢
(coe1‘𝐺) = (coe1‘(𝑋 − (𝐴‘𝑁))) | 
| 59 | 58 | fveq1i 6906 | . . . . 5
⊢
((coe1‘𝐺)‘1) = ((coe1‘(𝑋 − (𝐴‘𝑁)))‘1) | 
| 60 | 44 | a1i 11 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 61 |  | eqid 2736 | . . . . . . 7
⊢
(-g‘𝑅) = (-g‘𝑅) | 
| 62 | 5, 11, 20, 61 | coe1subfv 22270 | . . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐴‘𝑁) ∈ 𝐵) ∧ 1 ∈ ℕ0) →
((coe1‘(𝑋
−
(𝐴‘𝑁)))‘1) =
(((coe1‘𝑋)‘1)(-g‘𝑅)((coe1‘(𝐴‘𝑁))‘1))) | 
| 63 | 4, 13, 19, 60, 62 | syl31anc 1374 | . . . . 5
⊢ (𝜑 →
((coe1‘(𝑋
−
(𝐴‘𝑁)))‘1) =
(((coe1‘𝑋)‘1)(-g‘𝑅)((coe1‘(𝐴‘𝑁))‘1))) | 
| 64 | 59, 63 | eqtrid 2788 | . . . 4
⊢ (𝜑 →
((coe1‘𝐺)‘1) = (((coe1‘𝑋)‘1)(-g‘𝑅)((coe1‘(𝐴‘𝑁))‘1))) | 
| 65 | 42 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝜑 →
((1r‘𝑅)(
·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))𝑋)) = ((1r‘𝑅)( ·𝑠
‘𝑃)𝑋)) | 
| 66 | 5 | ply1sca 22255 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ NzRing → 𝑅 = (Scalar‘𝑃)) | 
| 67 | 2, 66 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | 
| 68 | 67 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝜑 → (1r‘𝑅) =
(1r‘(Scalar‘𝑃))) | 
| 69 | 68 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝜑 →
((1r‘𝑅)(
·𝑠 ‘𝑃)𝑋) =
((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)𝑋)) | 
| 70 | 5 | ply1lmod 22254 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) | 
| 71 | 4, 70 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ LMod) | 
| 72 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) | 
| 73 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) | 
| 74 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(1r‘(Scalar‘𝑃)) =
(1r‘(Scalar‘𝑃)) | 
| 75 | 11, 72, 73, 74 | lmodvs1 20889 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ LMod ∧ 𝑋 ∈ 𝐵) →
((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)𝑋) = 𝑋) | 
| 76 | 71, 13, 75 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 →
((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)𝑋) = 𝑋) | 
| 77 | 65, 69, 76 | 3eqtrd 2780 | . . . . . . . . 9
⊢ (𝜑 →
((1r‘𝑅)(
·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))𝑋)) = 𝑋) | 
| 78 | 77 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 →
(coe1‘((1r‘𝑅)( ·𝑠
‘𝑃)(1(.g‘(mulGrp‘𝑃))𝑋))) = (coe1‘𝑋)) | 
| 79 | 78 | fveq1d 6907 | . . . . . . 7
⊢ (𝜑 →
((coe1‘((1r‘𝑅)( ·𝑠
‘𝑃)(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = ((coe1‘𝑋)‘1)) | 
| 80 |  | eqid 2736 | . . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 81 | 15, 80 | ringidcl 20263 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐾) | 
| 82 | 4, 81 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐾) | 
| 83 |  | ply1rem.z | . . . . . . . . 9
⊢  0 =
(0g‘𝑅) | 
| 84 | 83, 15, 5, 10, 73, 38, 40 | coe1tmfv1 22278 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ 𝐾 ∧ 1 ∈
ℕ0) → ((coe1‘((1r‘𝑅)(
·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = (1r‘𝑅)) | 
| 85 | 4, 82, 60, 84 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 →
((coe1‘((1r‘𝑅)( ·𝑠
‘𝑃)(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = (1r‘𝑅)) | 
| 86 | 79, 85 | eqtr3d 2778 | . . . . . 6
⊢ (𝜑 →
((coe1‘𝑋)‘1) = (1r‘𝑅)) | 
| 87 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 88 | 5, 14, 15, 87 | coe1scl 22291 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ 𝐾) → (coe1‘(𝐴‘𝑁)) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 𝑁, (0g‘𝑅)))) | 
| 89 | 4, 18, 88 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 →
(coe1‘(𝐴‘𝑁)) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 𝑁, (0g‘𝑅)))) | 
| 90 | 89 | fveq1d 6907 | . . . . . . 7
⊢ (𝜑 →
((coe1‘(𝐴‘𝑁))‘1) = ((𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 𝑁, (0g‘𝑅)))‘1)) | 
| 91 |  | ax-1ne0 11225 | . . . . . . . . . . 11
⊢ 1 ≠
0 | 
| 92 |  | neeq1 3002 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ≠ 0 ↔ 1 ≠ 0)) | 
| 93 | 91, 92 | mpbiri 258 | . . . . . . . . . 10
⊢ (𝑥 = 1 → 𝑥 ≠ 0) | 
| 94 |  | ifnefalse 4536 | . . . . . . . . . 10
⊢ (𝑥 ≠ 0 → if(𝑥 = 0, 𝑁, (0g‘𝑅)) = (0g‘𝑅)) | 
| 95 | 93, 94 | syl 17 | . . . . . . . . 9
⊢ (𝑥 = 1 → if(𝑥 = 0, 𝑁, (0g‘𝑅)) = (0g‘𝑅)) | 
| 96 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
↦ if(𝑥 = 0, 𝑁, (0g‘𝑅))) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 𝑁, (0g‘𝑅))) | 
| 97 |  | fvex 6918 | . . . . . . . . 9
⊢
(0g‘𝑅) ∈ V | 
| 98 | 95, 96, 97 | fvmpt 7015 | . . . . . . . 8
⊢ (1 ∈
ℕ0 → ((𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 𝑁, (0g‘𝑅)))‘1) = (0g‘𝑅)) | 
| 99 | 44, 98 | ax-mp 5 | . . . . . . 7
⊢ ((𝑥 ∈ ℕ0
↦ if(𝑥 = 0, 𝑁, (0g‘𝑅)))‘1) =
(0g‘𝑅) | 
| 100 | 90, 99 | eqtrdi 2792 | . . . . . 6
⊢ (𝜑 →
((coe1‘(𝐴‘𝑁))‘1) = (0g‘𝑅)) | 
| 101 | 86, 100 | oveq12d 7450 | . . . . 5
⊢ (𝜑 →
(((coe1‘𝑋)‘1)(-g‘𝑅)((coe1‘(𝐴‘𝑁))‘1)) = ((1r‘𝑅)(-g‘𝑅)(0g‘𝑅))) | 
| 102 |  | ringgrp 20236 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 103 | 4, 102 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 104 | 15, 87, 61 | grpsubid1 19044 | . . . . . 6
⊢ ((𝑅 ∈ Grp ∧
(1r‘𝑅)
∈ 𝐾) →
((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)) = (1r‘𝑅)) | 
| 105 | 103, 82, 104 | syl2anc 584 | . . . . 5
⊢ (𝜑 →
((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)) = (1r‘𝑅)) | 
| 106 | 101, 105 | eqtrd 2776 | . . . 4
⊢ (𝜑 →
(((coe1‘𝑋)‘1)(-g‘𝑅)((coe1‘(𝐴‘𝑁))‘1)) = (1r‘𝑅)) | 
| 107 | 57, 64, 106 | 3eqtrd 2780 | . . 3
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) = (1r‘𝑅)) | 
| 108 |  | ply1rem.u | . . . 4
⊢ 𝑈 =
(Monic1p‘𝑅) | 
| 109 | 5, 11, 53, 25, 108, 80 | ismon1p 26183 | . . 3
⊢ (𝐺 ∈ 𝑈 ↔ (𝐺 ∈ 𝐵 ∧ 𝐺 ≠ (0g‘𝑃) ∧ ((coe1‘𝐺)‘(𝐷‘𝐺)) = (1r‘𝑅))) | 
| 110 | 23, 56, 107, 109 | syl3anbrc 1343 | . 2
⊢ (𝜑 → 𝐺 ∈ 𝑈) | 
| 111 | 1 | fveq2i 6908 | . . . . . . . . . 10
⊢ (𝑂‘𝐺) = (𝑂‘(𝑋 − (𝐴‘𝑁))) | 
| 112 | 111 | fveq1i 6906 | . . . . . . . . 9
⊢ ((𝑂‘𝐺)‘𝑥) = ((𝑂‘(𝑋 − (𝐴‘𝑁)))‘𝑥) | 
| 113 |  | ply1rem.o | . . . . . . . . . . 11
⊢ 𝑂 = (eval1‘𝑅) | 
| 114 |  | ply1rem.2 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 115 | 114 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ CRing) | 
| 116 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) | 
| 117 | 113, 10, 15, 5, 11, 115, 116 | evl1vard 22342 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘𝑥) = 𝑥)) | 
| 118 | 18 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑁 ∈ 𝐾) | 
| 119 | 113, 5, 15, 14, 11, 115, 118, 116 | evl1scad 22340 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑁) ∈ 𝐵 ∧ ((𝑂‘(𝐴‘𝑁))‘𝑥) = 𝑁)) | 
| 120 | 113, 5, 15, 11, 115, 116, 117, 119, 20, 61 | evl1subd 22347 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑋 − (𝐴‘𝑁)) ∈ 𝐵 ∧ ((𝑂‘(𝑋 − (𝐴‘𝑁)))‘𝑥) = (𝑥(-g‘𝑅)𝑁))) | 
| 121 | 120 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘(𝑋 − (𝐴‘𝑁)))‘𝑥) = (𝑥(-g‘𝑅)𝑁)) | 
| 122 | 112, 121 | eqtrid 2788 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐺)‘𝑥) = (𝑥(-g‘𝑅)𝑁)) | 
| 123 | 122 | eqeq1d 2738 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐺)‘𝑥) = 0 ↔ (𝑥(-g‘𝑅)𝑁) = 0 )) | 
| 124 | 103 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ Grp) | 
| 125 | 15, 83, 61 | grpsubeq0 19045 | . . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐾 ∧ 𝑁 ∈ 𝐾) → ((𝑥(-g‘𝑅)𝑁) = 0 ↔ 𝑥 = 𝑁)) | 
| 126 | 124, 116,
118, 125 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑥(-g‘𝑅)𝑁) = 0 ↔ 𝑥 = 𝑁)) | 
| 127 | 123, 126 | bitrd 279 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐺)‘𝑥) = 0 ↔ 𝑥 = 𝑁)) | 
| 128 |  | velsn 4641 | . . . . . 6
⊢ (𝑥 ∈ {𝑁} ↔ 𝑥 = 𝑁) | 
| 129 | 127, 128 | bitr4di 289 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐺)‘𝑥) = 0 ↔ 𝑥 ∈ {𝑁})) | 
| 130 | 129 | pm5.32da 579 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 0 ) ↔ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ {𝑁}))) | 
| 131 |  | eqid 2736 | . . . . . . 7
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) | 
| 132 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) | 
| 133 | 15 | fvexi 6919 | . . . . . . . 8
⊢ 𝐾 ∈ V | 
| 134 | 133 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ V) | 
| 135 | 113, 5, 131, 15 | evl1rhm 22337 | . . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) | 
| 136 | 114, 135 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) | 
| 137 | 11, 132 | rhmf 20486 | . . . . . . . . 9
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) | 
| 138 | 136, 137 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) | 
| 139 | 138, 23 | ffvelcdmd 7104 | . . . . . . 7
⊢ (𝜑 → (𝑂‘𝐺) ∈ (Base‘(𝑅 ↑s 𝐾))) | 
| 140 | 131, 15, 132, 2, 134, 139 | pwselbas 17535 | . . . . . 6
⊢ (𝜑 → (𝑂‘𝐺):𝐾⟶𝐾) | 
| 141 | 140 | ffnd 6736 | . . . . 5
⊢ (𝜑 → (𝑂‘𝐺) Fn 𝐾) | 
| 142 |  | fniniseg 7079 | . . . . 5
⊢ ((𝑂‘𝐺) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘𝐺) “ { 0 }) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 0 ))) | 
| 143 | 141, 142 | syl 17 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐺) “ { 0 }) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 0 ))) | 
| 144 | 18 | snssd 4808 | . . . . . 6
⊢ (𝜑 → {𝑁} ⊆ 𝐾) | 
| 145 | 144 | sseld 3981 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ {𝑁} → 𝑥 ∈ 𝐾)) | 
| 146 | 145 | pm4.71rd 562 | . . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑁} ↔ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ {𝑁}))) | 
| 147 | 130, 143,
146 | 3bitr4d 311 | . . 3
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐺) “ { 0 }) ↔ 𝑥 ∈ {𝑁})) | 
| 148 | 147 | eqrdv 2734 | . 2
⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) = {𝑁}) | 
| 149 | 110, 51, 148 | 3jca 1128 | 1
⊢ (𝜑 → (𝐺 ∈ 𝑈 ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ { 0 }) = {𝑁})) |