This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1rem

Description: The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout ). If a polynomial F is divided by the linear factor x - A , the remainder is equal to F ( A ) , the evaluation of the polynomial at A (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses 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 ply1rem ( 𝜑 → ( 𝐹 𝐸 𝐺 ) = ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 ply1rem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1rem.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 ply1rem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 ply1rem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 ply1rem.m ⊢ − = ( -g ‘ 𝑃 )
6 ply1rem.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
7 ply1rem.g ⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑁 ) )
8 ply1rem.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
9 ply1rem.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
10 ply1rem.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
11 ply1rem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
12 ply1rem.4 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
13 ply1rem.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
14 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
15 9 14 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
16 eqid ⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
17 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 1 2 3 4 5 6 7 8 9 10 11 16 17 18 ply1remlem ⊢ ( 𝜑 → ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) = 1 ∧ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { ( 0g ‘ 𝑅 ) } ) = { 𝑁 } ) )
20 19 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ 𝑅 ) )
21 eqid ⊢ ( Unic1p ‘ 𝑅 ) = ( Unic1p ‘ 𝑅 )
22 21 16 mon1puc1p ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ) → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
23 15 20 22 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
24 13 1 2 21 17 r1pdeglt ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) )
25 15 12 23 24 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) )
26 19 simp2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) = 1 )
27 25 26 breqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) < 1 )
28 1e0p1 ⊢ 1 = ( 0 + 1 )
29 27 28 breqtrdi ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( 0 + 1 ) )
30 0nn0 ⊢ 0 ∈ ℕ0
31 nn0leltp1 ⊢ ( ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( 0 + 1 ) ) )
32 30 31 mpan2 ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( 0 + 1 ) ) )
33 29 32 syl5ibrcom ⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 ) )
34 elsni ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ { -∞ } → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ )
35 0xr ⊢ 0 ∈ ℝ*
36 mnfle ⊢ ( 0 ∈ ℝ* → -∞ ≤ 0 )
37 35 36 ax-mp ⊢ -∞ ≤ 0
38 34 37 eqbrtrdi ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ { -∞ } → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 )
39 38 a1i ⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ { -∞ } → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 ) )
40 13 1 2 21 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐹 𝐸 𝐺 ) ∈ 𝐵 )
41 15 12 23 40 syl3anc ⊢ ( 𝜑 → ( 𝐹 𝐸 𝐺 ) ∈ 𝐵 )
42 17 1 2 deg1cl ⊢ ( ( 𝐹 𝐸 𝐺 ) ∈ 𝐵 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) )
43 41 42 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) )
44 elun ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∨ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ { -∞ } ) )
45 43 44 sylib ⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∨ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ { -∞ } ) )
46 33 39 45 mpjaod ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 )
47 17 1 2 6 deg1le0 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 𝐸 𝐺 ) ∈ 𝐵 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 ↔ ( 𝐹 𝐸 𝐺 ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) ) )
48 15 41 47 syl2anc ⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 0 ↔ ( 𝐹 𝐸 𝐺 ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) ) )
49 46 48 mpbid ⊢ ( 𝜑 → ( 𝐹 𝐸 𝐺 ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) )
50 eqid ⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
51 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
52 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
53 1 2 21 50 13 51 52 r1pid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → 𝐹 = ( ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) )
54 15 12 23 53 syl3anc ⊢ ( 𝜑 → 𝐹 = ( ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) )
55 54 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) = ( 𝑂 ‘ ( ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) )
56 eqid ⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
57 8 1 56 3 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
58 10 57 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
59 rhmghm ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐾 ) ) )
60 58 59 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐾 ) ) )
61 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
62 15 61 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
63 50 1 2 21 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 )
64 15 12 23 63 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 )
65 1 2 16 mon1pcl ⊢ ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) → 𝐺 ∈ 𝐵 )
66 20 65 syl ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
67 2 51 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ∈ 𝐵 )
68 62 64 66 67 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ∈ 𝐵 )
69 eqid ⊢ ( +g ‘ ( 𝑅 ↑s 𝐾 ) ) = ( +g ‘ ( 𝑅 ↑s 𝐾 ) )
70 2 52 69 ghmlin ⊢ ( ( 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐾 ) ) ∧ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ∈ 𝐵 ∧ ( 𝐹 𝐸 𝐺 ) ∈ 𝐵 ) → ( 𝑂 ‘ ( ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ( +g ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) )
71 60 68 41 70 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ( +g ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) )
72 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐾 ) )
73 3 fvexi ⊢ 𝐾 ∈ V
74 73 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
75 2 72 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
76 58 75 syl ⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
77 76 68 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
78 76 41 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
79 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
80 56 72 9 74 77 78 79 69 pwsplusgval ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ( +g ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) )
81 55 71 80 3eqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) = ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) )
82 81 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) = ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑁 ) )
83 56 3 72 9 74 77 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) : 𝐾 ⟶ 𝐾 )
84 83 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) Fn 𝐾 )
85 56 3 72 9 74 78 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) : 𝐾 ⟶ 𝐾 )
86 85 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) Fn 𝐾 )
87 fnfvof ⊢ ( ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) Fn 𝐾 ∧ ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) Fn 𝐾 ) ∧ ( 𝐾 ∈ V ∧ 𝑁 ∈ 𝐾 ) ) → ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑁 ) = ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑁 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ) )
88 84 86 74 11 87 syl22anc ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑁 ) = ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑁 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ) )
89 eqid ⊢ ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) = ( .r ‘ ( 𝑅 ↑s 𝐾 ) )
90 2 51 89 rhmmul ⊢ ( ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) ∧ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝐺 ) ) )
91 58 64 66 90 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝐺 ) ) )
92 76 64 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
93 76 66 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
94 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
95 56 72 9 74 92 93 94 89 pwsmulrval ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) )
96 91 95 eqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) )
97 96 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑁 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑁 ) )
98 56 3 72 9 74 92 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) : 𝐾 ⟶ 𝐾 )
99 98 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) Fn 𝐾 )
100 56 3 72 9 74 93 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) : 𝐾 ⟶ 𝐾 )
101 100 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) Fn 𝐾 )
102 fnfvof ⊢ ( ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) Fn 𝐾 ∧ ( 𝑂 ‘ 𝐺 ) Fn 𝐾 ) ∧ ( 𝐾 ∈ V ∧ 𝑁 ∈ 𝐾 ) ) → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑁 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) ) )
103 99 101 74 11 102 syl22anc ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑁 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) ) )
104 snidg ⊢ ( 𝑁 ∈ 𝐾 → 𝑁 ∈ { 𝑁 } )
105 11 104 syl ⊢ ( 𝜑 → 𝑁 ∈ { 𝑁 } )
106 19 simp3d ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { ( 0g ‘ 𝑅 ) } ) = { 𝑁 } )
107 105 106 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { ( 0g ‘ 𝑅 ) } ) )
108 fniniseg ⊢ ( ( 𝑂 ‘ 𝐺 ) Fn 𝐾 → ( 𝑁 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝑁 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) ) )
109 101 108 syl ⊢ ( 𝜑 → ( 𝑁 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝑁 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) ) )
110 107 109 mpbid ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) ) )
111 110 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) )
112 111 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
113 98 11 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ∈ 𝐾 )
114 3 94 18 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ∈ 𝐾 ) → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
115 15 113 114 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
116 112 115 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑁 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑁 ) ) = ( 0g ‘ 𝑅 ) )
117 97 103 116 3eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑁 ) = ( 0g ‘ 𝑅 ) )
118 117 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑁 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ) )
119 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
120 15 119 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
121 85 11 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ∈ 𝐾 )
122 3 79 18 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ∈ 𝐾 ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ) = ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) )
123 120 121 122 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) ) = ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) )
124 88 118 123 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑁 ) = ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) )
125 49 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) = ( 𝑂 ‘ ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) ) )
126 eqid ⊢ ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) = ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) )
127 126 2 1 3 coe1f ⊢ ( ( 𝐹 𝐸 𝐺 ) ∈ 𝐵 → ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) : ℕ0 ⟶ 𝐾 )
128 41 127 syl ⊢ ( 𝜑 → ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) : ℕ0 ⟶ 𝐾 )
129 ffvelcdm ⊢ ( ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) : ℕ0 ⟶ 𝐾 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ∈ 𝐾 )
130 128 30 129 sylancl ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ∈ 𝐾 )
131 8 1 3 6 evl1sca ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ∈ 𝐾 ) → ( 𝑂 ‘ ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) ) = ( 𝐾 × { ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) } ) )
132 10 130 131 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) ) = ( 𝐾 × { ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) } ) )
133 125 132 eqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) = ( 𝐾 × { ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) } ) )
134 133 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝐾 × { ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) } ) ‘ 𝑁 ) )
135 fvex ⊢ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ∈ V
136 135 fvconst2 ⊢ ( 𝑁 ∈ 𝐾 → ( ( 𝐾 × { ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) } ) ‘ 𝑁 ) = ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) )
137 11 136 syl ⊢ ( 𝜑 → ( ( 𝐾 × { ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) } ) ‘ 𝑁 ) = ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) )
138 134 137 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑁 ) = ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) )
139 82 124 138 3eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) )
140 139 fveq2d ⊢ ( 𝜑 → ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 0 ) ) )
141 49 140 eqtr4d ⊢ ( 𝜑 → ( 𝐹 𝐸 𝐺 ) = ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) )