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