MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ply1rem Structured version   Visualization version   GIF version

Theorem ply1rem 25400
Description: The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 16323). If a polynomial 𝐹 is divided by the linear factor 𝑥𝐴, the remainder is equal to 𝐹(𝐴), the evaluation of the polynomial at 𝐴 (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015.)
Hypotheses
Ref Expression
ply1rem.p 𝑃 = (Poly1𝑅)
ply1rem.b 𝐵 = (Base‘𝑃)
ply1rem.k 𝐾 = (Base‘𝑅)
ply1rem.x 𝑋 = (var1𝑅)
ply1rem.m = (-g𝑃)
ply1rem.a 𝐴 = (algSc‘𝑃)
ply1rem.g 𝐺 = (𝑋 (𝐴𝑁))
ply1rem.o 𝑂 = (eval1𝑅)
ply1rem.1 (𝜑𝑅 ∈ NzRing)
ply1rem.2 (𝜑𝑅 ∈ CRing)
ply1rem.3 (𝜑𝑁𝐾)
ply1rem.4 (𝜑𝐹𝐵)
ply1rem.e 𝐸 = (rem1p𝑅)
Assertion
Ref Expression
ply1rem (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((𝑂𝐹)‘𝑁)))

Proof of Theorem ply1rem
StepHypRef Expression
1 ply1rem.1 . . . . . . . . 9 (𝜑𝑅 ∈ NzRing)
2 nzrring 20604 . . . . . . . . 9 (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
31, 2syl 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 2737 . . . . . . . . . . 11 (Monic1p𝑅) = (Monic1p𝑅)
16 eqid 2737 . . . . . . . . . . 11 ( deg1𝑅) = ( deg1𝑅)
17 eqid 2737 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
185, 6, 7, 8, 9, 10, 11, 12, 1, 13, 14, 15, 16, 17ply1remlem 25399 . . . . . . . . . 10 (𝜑 → (𝐺 ∈ (Monic1p𝑅) ∧ (( deg1𝑅)‘𝐺) = 1 ∧ ((𝑂𝐺) “ {(0g𝑅)}) = {𝑁}))
1918simp1d 1141 . . . . . . . . 9 (𝜑𝐺 ∈ (Monic1p𝑅))
20 eqid 2737 . . . . . . . . . 10 (Unic1p𝑅) = (Unic1p𝑅)
2120, 15mon1puc1p 25387 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐺 ∈ (Monic1p𝑅)) → 𝐺 ∈ (Unic1p𝑅))
223, 19, 21syl2anc 584 . . . . . . . 8 (𝜑𝐺 ∈ (Unic1p𝑅))
23 ply1rem.e . . . . . . . . 9 𝐸 = (rem1p𝑅)
2423, 5, 6, 20, 16r1pdeglt 25395 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐹𝐵𝐺 ∈ (Unic1p𝑅)) → (( deg1𝑅)‘(𝐹𝐸𝐺)) < (( deg1𝑅)‘𝐺))
253, 4, 22, 24syl3anc 1370 . . . . . . 7 (𝜑 → (( deg1𝑅)‘(𝐹𝐸𝐺)) < (( deg1𝑅)‘𝐺))
2618simp2d 1142 . . . . . . 7 (𝜑 → (( deg1𝑅)‘𝐺) = 1)
2725, 26breqtrd 5113 . . . . . 6 (𝜑 → (( deg1𝑅)‘(𝐹𝐸𝐺)) < 1)
28 1e0p1 12552 . . . . . 6 1 = (0 + 1)
2927, 28breqtrdi 5128 . . . . 5 (𝜑 → (( deg1𝑅)‘(𝐹𝐸𝐺)) < (0 + 1))
30 0nn0 12321 . . . . . 6 0 ∈ ℕ0
31 nn0leltp1 12452 . . . . . 6 (((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 ∧ 0 ∈ ℕ0) → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (( deg1𝑅)‘(𝐹𝐸𝐺)) < (0 + 1)))
3230, 31mpan2 688 . . . . 5 ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (( deg1𝑅)‘(𝐹𝐸𝐺)) < (0 + 1)))
3329, 32syl5ibrcom 246 . . . 4 (𝜑 → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 → (( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0))
34 elsni 4588 . . . . . 6 ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞} → (( deg1𝑅)‘(𝐹𝐸𝐺)) = -∞)
35 0xr 11095 . . . . . . 7 0 ∈ ℝ*
36 mnfle 12943 . . . . . . 7 (0 ∈ ℝ* → -∞ ≤ 0)
3735, 36ax-mp 5 . . . . . 6 -∞ ≤ 0
3834, 37eqbrtrdi 5126 . . . . 5 ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞} → (( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0)
3938a1i 11 . . . 4 (𝜑 → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞} → (( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0))
4023, 5, 6, 20r1pcl 25394 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐹𝐵𝐺 ∈ (Unic1p𝑅)) → (𝐹𝐸𝐺) ∈ 𝐵)
413, 4, 22, 40syl3anc 1370 . . . . . 6 (𝜑 → (𝐹𝐸𝐺) ∈ 𝐵)
4216, 5, 6deg1cl 25320 . . . . . 6 ((𝐹𝐸𝐺) ∈ 𝐵 → (( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}))
4341, 42syl 17 . . . . 5 (𝜑 → (( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}))
44 elun 4094 . . . . 5 ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}) ↔ ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ (( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞}))
4543, 44sylib 217 . . . 4 (𝜑 → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ (( deg1𝑅)‘(𝐹𝐸𝐺)) ∈ {-∞}))
4633, 39, 45mpjaod 857 . . 3 (𝜑 → (( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0)
4716, 5, 6, 10deg1le0 25348 . . . 4 ((𝑅 ∈ Ring ∧ (𝐹𝐸𝐺) ∈ 𝐵) → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (𝐹𝐸𝐺) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))))
483, 41, 47syl2anc 584 . . 3 (𝜑 → ((( deg1𝑅)‘(𝐹𝐸𝐺)) ≤ 0 ↔ (𝐹𝐸𝐺) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))))
4946, 48mpbid 231 . 2 (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0)))
50 eqid 2737 . . . . . . . . 9 (quot1p𝑅) = (quot1p𝑅)
51 eqid 2737 . . . . . . . . 9 (.r𝑃) = (.r𝑃)
52 eqid 2737 . . . . . . . . 9 (+g𝑃) = (+g𝑃)
535, 6, 20, 50, 23, 51, 52r1pid 25396 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐹𝐵𝐺 ∈ (Unic1p𝑅)) → 𝐹 = (((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)(+g𝑃)(𝐹𝐸𝐺)))
543, 4, 22, 53syl3anc 1370 . . . . . . 7 (𝜑𝐹 = (((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)(+g𝑃)(𝐹𝐸𝐺)))
5554fveq2d 6815 . . . . . 6 (𝜑 → (𝑂𝐹) = (𝑂‘(((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)(+g𝑃)(𝐹𝐸𝐺))))
56 eqid 2737 . . . . . . . . . 10 (𝑅s 𝐾) = (𝑅s 𝐾)
5712, 5, 56, 7evl1rhm 21570 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)))
5813, 57syl 17 . . . . . . . 8 (𝜑𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)))
59 rhmghm 20037 . . . . . . . 8 (𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)) → 𝑂 ∈ (𝑃 GrpHom (𝑅s 𝐾)))
6058, 59syl 17 . . . . . . 7 (𝜑𝑂 ∈ (𝑃 GrpHom (𝑅s 𝐾)))
615ply1ring 21491 . . . . . . . . 9 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
623, 61syl 17 . . . . . . . 8 (𝜑𝑃 ∈ Ring)
6350, 5, 6, 20q1pcl 25392 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐹𝐵𝐺 ∈ (Unic1p𝑅)) → (𝐹(quot1p𝑅)𝐺) ∈ 𝐵)
643, 4, 22, 63syl3anc 1370 . . . . . . . 8 (𝜑 → (𝐹(quot1p𝑅)𝐺) ∈ 𝐵)
655, 6, 15mon1pcl 25381 . . . . . . . . 9 (𝐺 ∈ (Monic1p𝑅) → 𝐺𝐵)
6619, 65syl 17 . . . . . . . 8 (𝜑𝐺𝐵)
676, 51ringcl 19868 . . . . . . . 8 ((𝑃 ∈ Ring ∧ (𝐹(quot1p𝑅)𝐺) ∈ 𝐵𝐺𝐵) → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) ∈ 𝐵)
6862, 64, 66, 67syl3anc 1370 . . . . . . 7 (𝜑 → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) ∈ 𝐵)
69 eqid 2737 . . . . . . . 8 (+g‘(𝑅s 𝐾)) = (+g‘(𝑅s 𝐾))
706, 52, 69ghmlin 18908 . . . . . . 7 ((𝑂 ∈ (𝑃 GrpHom (𝑅s 𝐾)) ∧ ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) ∈ 𝐵 ∧ (𝐹𝐸𝐺) ∈ 𝐵) → (𝑂‘(((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)(+g𝑃)(𝐹𝐸𝐺))) = ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))(+g‘(𝑅s 𝐾))(𝑂‘(𝐹𝐸𝐺))))
7160, 68, 41, 70syl3anc 1370 . . . . . 6 (𝜑 → (𝑂‘(((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)(+g𝑃)(𝐹𝐸𝐺))) = ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))(+g‘(𝑅s 𝐾))(𝑂‘(𝐹𝐸𝐺))))
72 eqid 2737 . . . . . . 7 (Base‘(𝑅s 𝐾)) = (Base‘(𝑅s 𝐾))
737fvexi 6825 . . . . . . . 8 𝐾 ∈ V
7473a1i 11 . . . . . . 7 (𝜑𝐾 ∈ V)
756, 72rhmf 20038 . . . . . . . . 9 (𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅s 𝐾)))
7658, 75syl 17 . . . . . . . 8 (𝜑𝑂:𝐵⟶(Base‘(𝑅s 𝐾)))
7776, 68ffvelcdmd 7001 . . . . . . 7 (𝜑 → (𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∈ (Base‘(𝑅s 𝐾)))
7876, 41ffvelcdmd 7001 . . . . . . 7 (𝜑 → (𝑂‘(𝐹𝐸𝐺)) ∈ (Base‘(𝑅s 𝐾)))
79 eqid 2737 . . . . . . 7 (+g𝑅) = (+g𝑅)
8056, 72, 1, 74, 77, 78, 79, 69pwsplusgval 17271 . . . . . 6 (𝜑 → ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))(+g‘(𝑅s 𝐾))(𝑂‘(𝐹𝐸𝐺))) = ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∘f (+g𝑅)(𝑂‘(𝐹𝐸𝐺))))
8155, 71, 803eqtrd 2781 . . . . 5 (𝜑 → (𝑂𝐹) = ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∘f (+g𝑅)(𝑂‘(𝐹𝐸𝐺))))
8281fveq1d 6813 . . . 4 (𝜑 → ((𝑂𝐹)‘𝑁) = (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∘f (+g𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁))
8356, 7, 72, 1, 74, 77pwselbas 17270 . . . . . . 7 (𝜑 → (𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)):𝐾𝐾)
8483ffnd 6638 . . . . . 6 (𝜑 → (𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) Fn 𝐾)
8556, 7, 72, 1, 74, 78pwselbas 17270 . . . . . . 7 (𝜑 → (𝑂‘(𝐹𝐸𝐺)):𝐾𝐾)
8685ffnd 6638 . . . . . 6 (𝜑 → (𝑂‘(𝐹𝐸𝐺)) Fn 𝐾)
87 fnfvof 7590 . . . . . 6 ((((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) Fn 𝐾 ∧ (𝑂‘(𝐹𝐸𝐺)) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑁𝐾)) → (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∘f (+g𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁) = (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))‘𝑁)(+g𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)))
8884, 86, 74, 14, 87syl22anc 836 . . . . 5 (𝜑 → (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∘f (+g𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁) = (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))‘𝑁)(+g𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)))
89 eqid 2737 . . . . . . . . . . 11 (.r‘(𝑅s 𝐾)) = (.r‘(𝑅s 𝐾))
906, 51, 89rhmmul 20039 . . . . . . . . . 10 ((𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)) ∧ (𝐹(quot1p𝑅)𝐺) ∈ 𝐵𝐺𝐵) → (𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p𝑅)𝐺))(.r‘(𝑅s 𝐾))(𝑂𝐺)))
9158, 64, 66, 90syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p𝑅)𝐺))(.r‘(𝑅s 𝐾))(𝑂𝐺)))
9276, 64ffvelcdmd 7001 . . . . . . . . . 10 (𝜑 → (𝑂‘(𝐹(quot1p𝑅)𝐺)) ∈ (Base‘(𝑅s 𝐾)))
9376, 66ffvelcdmd 7001 . . . . . . . . . 10 (𝜑 → (𝑂𝐺) ∈ (Base‘(𝑅s 𝐾)))
94 eqid 2737 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
9556, 72, 1, 74, 92, 93, 94, 89pwsmulrval 17272 . . . . . . . . 9 (𝜑 → ((𝑂‘(𝐹(quot1p𝑅)𝐺))(.r‘(𝑅s 𝐾))(𝑂𝐺)) = ((𝑂‘(𝐹(quot1p𝑅)𝐺)) ∘f (.r𝑅)(𝑂𝐺)))
9691, 95eqtrd 2777 . . . . . . . 8 (𝜑 → (𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p𝑅)𝐺)) ∘f (.r𝑅)(𝑂𝐺)))
9796fveq1d 6813 . . . . . . 7 (𝜑 → ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))‘𝑁) = (((𝑂‘(𝐹(quot1p𝑅)𝐺)) ∘f (.r𝑅)(𝑂𝐺))‘𝑁))
9856, 7, 72, 1, 74, 92pwselbas 17270 . . . . . . . . 9 (𝜑 → (𝑂‘(𝐹(quot1p𝑅)𝐺)):𝐾𝐾)
9998ffnd 6638 . . . . . . . 8 (𝜑 → (𝑂‘(𝐹(quot1p𝑅)𝐺)) Fn 𝐾)
10056, 7, 72, 1, 74, 93pwselbas 17270 . . . . . . . . 9 (𝜑 → (𝑂𝐺):𝐾𝐾)
101100ffnd 6638 . . . . . . . 8 (𝜑 → (𝑂𝐺) Fn 𝐾)
102 fnfvof 7590 . . . . . . . 8 ((((𝑂‘(𝐹(quot1p𝑅)𝐺)) Fn 𝐾 ∧ (𝑂𝐺) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑁𝐾)) → (((𝑂‘(𝐹(quot1p𝑅)𝐺)) ∘f (.r𝑅)(𝑂𝐺))‘𝑁) = (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)((𝑂𝐺)‘𝑁)))
10399, 101, 74, 14, 102syl22anc 836 . . . . . . 7 (𝜑 → (((𝑂‘(𝐹(quot1p𝑅)𝐺)) ∘f (.r𝑅)(𝑂𝐺))‘𝑁) = (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)((𝑂𝐺)‘𝑁)))
104 snidg 4605 . . . . . . . . . . . . 13 (𝑁𝐾𝑁 ∈ {𝑁})
10514, 104syl 17 . . . . . . . . . . . 12 (𝜑𝑁 ∈ {𝑁})
10618simp3d 1143 . . . . . . . . . . . 12 (𝜑 → ((𝑂𝐺) “ {(0g𝑅)}) = {𝑁})
107105, 106eleqtrrd 2841 . . . . . . . . . . 11 (𝜑𝑁 ∈ ((𝑂𝐺) “ {(0g𝑅)}))
108 fniniseg 6976 . . . . . . . . . . . 12 ((𝑂𝐺) Fn 𝐾 → (𝑁 ∈ ((𝑂𝐺) “ {(0g𝑅)}) ↔ (𝑁𝐾 ∧ ((𝑂𝐺)‘𝑁) = (0g𝑅))))
109101, 108syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ((𝑂𝐺) “ {(0g𝑅)}) ↔ (𝑁𝐾 ∧ ((𝑂𝐺)‘𝑁) = (0g𝑅))))
110107, 109mpbid 231 . . . . . . . . . 10 (𝜑 → (𝑁𝐾 ∧ ((𝑂𝐺)‘𝑁) = (0g𝑅)))
111110simprd 496 . . . . . . . . 9 (𝜑 → ((𝑂𝐺)‘𝑁) = (0g𝑅))
112111oveq2d 7331 . . . . . . . 8 (𝜑 → (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)((𝑂𝐺)‘𝑁)) = (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)(0g𝑅)))
11398, 14ffvelcdmd 7001 . . . . . . . . 9 (𝜑 → ((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁) ∈ 𝐾)
1147, 94, 17ringrz 19895 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ ((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁) ∈ 𝐾) → (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)(0g𝑅)) = (0g𝑅))
1153, 113, 114syl2anc 584 . . . . . . . 8 (𝜑 → (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)(0g𝑅)) = (0g𝑅))
116112, 115eqtrd 2777 . . . . . . 7 (𝜑 → (((𝑂‘(𝐹(quot1p𝑅)𝐺))‘𝑁)(.r𝑅)((𝑂𝐺)‘𝑁)) = (0g𝑅))
11797, 103, 1163eqtrd 2781 . . . . . 6 (𝜑 → ((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))‘𝑁) = (0g𝑅))
118117oveq1d 7330 . . . . 5 (𝜑 → (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))‘𝑁)(+g𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)) = ((0g𝑅)(+g𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)))
119 ringgrp 19856 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
1203, 119syl 17 . . . . . 6 (𝜑𝑅 ∈ Grp)
12185, 14ffvelcdmd 7001 . . . . . 6 (𝜑 → ((𝑂‘(𝐹𝐸𝐺))‘𝑁) ∈ 𝐾)
1227, 79, 17grplid 18678 . . . . . 6 ((𝑅 ∈ Grp ∧ ((𝑂‘(𝐹𝐸𝐺))‘𝑁) ∈ 𝐾) → ((0g𝑅)(+g𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)) = ((𝑂‘(𝐹𝐸𝐺))‘𝑁))
123120, 121, 122syl2anc 584 . . . . 5 (𝜑 → ((0g𝑅)(+g𝑅)((𝑂‘(𝐹𝐸𝐺))‘𝑁)) = ((𝑂‘(𝐹𝐸𝐺))‘𝑁))
12488, 118, 1233eqtrd 2781 . . . 4 (𝜑 → (((𝑂‘((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)) ∘f (+g𝑅)(𝑂‘(𝐹𝐸𝐺)))‘𝑁) = ((𝑂‘(𝐹𝐸𝐺))‘𝑁))
12549fveq2d 6815 . . . . . . 7 (𝜑 → (𝑂‘(𝐹𝐸𝐺)) = (𝑂‘(𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))))
126 eqid 2737 . . . . . . . . . . 11 (coe1‘(𝐹𝐸𝐺)) = (coe1‘(𝐹𝐸𝐺))
127126, 6, 5, 7coe1f 21454 . . . . . . . . . 10 ((𝐹𝐸𝐺) ∈ 𝐵 → (coe1‘(𝐹𝐸𝐺)):ℕ0𝐾)
12841, 127syl 17 . . . . . . . . 9 (𝜑 → (coe1‘(𝐹𝐸𝐺)):ℕ0𝐾)
129 ffvelcdm 6998 . . . . . . . . 9 (((coe1‘(𝐹𝐸𝐺)):ℕ0𝐾 ∧ 0 ∈ ℕ0) → ((coe1‘(𝐹𝐸𝐺))‘0) ∈ 𝐾)
130128, 30, 129sylancl 586 . . . . . . . 8 (𝜑 → ((coe1‘(𝐹𝐸𝐺))‘0) ∈ 𝐾)
13112, 5, 7, 10evl1sca 21572 . . . . . . . 8 ((𝑅 ∈ CRing ∧ ((coe1‘(𝐹𝐸𝐺))‘0) ∈ 𝐾) → (𝑂‘(𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))) = (𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)}))
13213, 130, 131syl2anc 584 . . . . . . 7 (𝜑 → (𝑂‘(𝐴‘((coe1‘(𝐹𝐸𝐺))‘0))) = (𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)}))
133125, 132eqtrd 2777 . . . . . 6 (𝜑 → (𝑂‘(𝐹𝐸𝐺)) = (𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)}))
134133fveq1d 6813 . . . . 5 (𝜑 → ((𝑂‘(𝐹𝐸𝐺))‘𝑁) = ((𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})‘𝑁))
135 fvex 6824 . . . . . . 7 ((coe1‘(𝐹𝐸𝐺))‘0) ∈ V
136135fvconst2 7118 . . . . . 6 (𝑁𝐾 → ((𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0))
13714, 136syl 17 . . . . 5 (𝜑 → ((𝐾 × {((coe1‘(𝐹𝐸𝐺))‘0)})‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0))
138134, 137eqtrd 2777 . . . 4 (𝜑 → ((𝑂‘(𝐹𝐸𝐺))‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0))
13982, 124, 1383eqtrd 2781 . . 3 (𝜑 → ((𝑂𝐹)‘𝑁) = ((coe1‘(𝐹𝐸𝐺))‘0))
140139fveq2d 6815 . 2 (𝜑 → (𝐴‘((𝑂𝐹)‘𝑁)) = (𝐴‘((coe1‘(𝐹𝐸𝐺))‘0)))
14149, 140eqtr4d 2780 1 (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((𝑂𝐹)‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844   = wceq 1540  wcel 2105  Vcvv 3441  cun 3895  {csn 4571   class class class wbr 5087   × cxp 5605  ccnv 5606  cima 5610   Fn wfn 6460  wf 6461  cfv 6465  (class class class)co 7315  f cof 7571  0cc0 10944  1c1 10945   + caddc 10947  -∞cmnf 11080  *cxr 11081   < clt 11082  cle 11083  0cn0 12306  Basecbs 16982  +gcplusg 17032  .rcmulr 17033  0gc0g 17220  s cpws 17227  Grpcgrp 18646  -gcsg 18648   GrpHom cghm 18900  Ringcrg 19851  CRingccrg 19852   RingHom crh 20024  NzRingcnzr 20600  algSccascl 21131  var1cv1 21419  Poly1cpl1 21420  coe1cco1 21421  eval1ce1 21552   deg1 cdg1 25288  Monic1pcmn1 25362  Unic1pcuc1p 25363  quot1pcq1p 25364  rem1pcr1p 25365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022  ax-addf 11023  ax-mulf 11024
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-of 7573  df-ofr 7574  df-om 7758  df-1st 7876  df-2nd 7877  df-supp 8025  df-tpos 8089  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-er 8546  df-map 8665  df-pm 8666  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-fsupp 9199  df-sup 9271  df-oi 9339  df-card 9768  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-z 12393  df-dec 12511  df-uz 12656  df-fz 13313  df-fzo 13456  df-seq 13795  df-hash 14118  df-struct 16918  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-mulr 17046  df-starv 17047  df-sca 17048  df-vsca 17049  df-ip 17050  df-tset 17051  df-ple 17052  df-ds 17054  df-unif 17055  df-hom 17056  df-cco 17057  df-0g 17222  df-gsum 17223  df-prds 17228  df-pws 17230  df-mre 17365  df-mrc 17366  df-acs 17368  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-mhm 18500  df-submnd 18501  df-grp 18649  df-minusg 18650  df-sbg 18651  df-mulg 18770  df-subg 18821  df-ghm 18901  df-cntz 18992  df-cmn 19456  df-abl 19457  df-mgp 19789  df-ur 19806  df-srg 19810  df-ring 19853  df-cring 19854  df-oppr 19930  df-dvdsr 19951  df-unit 19952  df-invr 19982  df-rnghom 20027  df-subrg 20094  df-lmod 20197  df-lss 20266  df-lsp 20306  df-nzr 20601  df-rlreg 20626  df-cnfld 20670  df-assa 21132  df-asp 21133  df-ascl 21134  df-psr 21184  df-mvr 21185  df-mpl 21186  df-opsr 21188  df-evls 21354  df-evl 21355  df-psr1 21423  df-vr1 21424  df-ply1 21425  df-coe1 21426  df-evl1 21554  df-mdeg 25289  df-deg1 25290  df-mon1 25367  df-uc1p 25368  df-q1p 25369  df-r1p 25370
This theorem is referenced by:  facth1  25401
  Copyright terms: Public domain W3C validator