Theorem fta1glem2

Description: Lemma for fta1g . (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	fta1g.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	fta1g.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	fta1g.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	fta1g.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	fta1g.w	⊢ 𝑊 = ( 0g ‘ 𝑅 )
	fta1g.z	⊢ 0 = ( 0g ‘ 𝑃 )
	fta1g.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	fta1g.2	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	fta1glem.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	fta1glem.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	fta1glem.m	⊢ − = ( -g ‘ 𝑃 )
	fta1glem.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	fta1glem.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑇 ) )
	fta1glem.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	fta1glem.4	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝑁 + 1 ) )
	fta1glem.5	⊢ ( 𝜑 → 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) )
	fta1glem.6	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝐵 ( ( 𝐷 ‘ 𝑔 ) = 𝑁 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑔 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑔 ) ) )
Assertion	fta1glem2	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fta1g.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		fta1g.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		fta1g.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
4		fta1g.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
5		fta1g.w	⊢ 𝑊 = ( 0g ‘ 𝑅 )
6		fta1g.z	⊢ 0 = ( 0g ‘ 𝑃 )
7		fta1g.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
8		fta1g.2	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		fta1glem.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
10		fta1glem.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
11		fta1glem.m	⊢ − = ( -g ‘ 𝑃 )
12		fta1glem.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
13		fta1glem.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑇 ) )
14		fta1glem.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15		fta1glem.4	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝑁 + 1 ) )
16		fta1glem.5	⊢ ( 𝜑 → 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) )
17		fta1glem.6	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝐵 ( ( 𝐷 ‘ 𝑔 ) = 𝑁 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑔 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑔 ) ) )
18		eqid	⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
19		eqid	⊢ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐾 ) )
20	9	fvexi	⊢ 𝐾 ∈ V
21	20	a1i	⊢ ( 𝜑 → 𝐾 ∈ V )
22		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
23	22	simplbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
24	7 23	syl	⊢ ( 𝜑 → 𝑅 ∈ CRing )
25	4 1 18 9	evl1rhm	⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
26	24 25	syl	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
27	2 19	rhmf	⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
28	26 27	syl	⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
29	28 8	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
30	18 9 19 7 21 29	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) : 𝐾 ⟶ 𝐾 )
31	30	ffnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) Fn 𝐾 )
32		fniniseg	⊢ ( ( 𝑂 ‘ 𝐹 ) Fn 𝐾 → ( 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ ( 𝑇 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) ) )
33	31 32	syl	⊢ ( 𝜑 → ( 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ ( 𝑇 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) ) )
34	16 33	mpbid	⊢ ( 𝜑 → ( 𝑇 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) )
35	34	simprd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 )
36	22	simprbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
37		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
38	36 37	syl	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ NzRing )
39	7 38	syl	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
40	34	simpld	⊢ ( 𝜑 → 𝑇 ∈ 𝐾 )
41		eqid	⊢ ( ∥r ‘ 𝑃 ) = ( ∥r ‘ 𝑃 )
42	1 2 9 10 11 12 13 4 39 24 40 8 5 41	facth1	⊢ ( 𝜑 → ( 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) )
43	35 42	mpbird	⊢ ( 𝜑 → 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 )
44		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
45	39 44	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
46		eqid	⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
47	1 2 9 10 11 12 13 4 39 24 40 46 3 5	ply1remlem	⊢ ( 𝜑 → ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝐺 ) = 1 ∧ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 𝑊 } ) = { 𝑇 } ) )
48	47	simp1d	⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ 𝑅 ) )
49		eqid	⊢ ( Unic1p ‘ 𝑅 ) = ( Unic1p ‘ 𝑅 )
50	49 46	mon1puc1p	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ) → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
51	45 48 50	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
52		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
53		eqid	⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
54	1 41 2 49 52 53	dvdsq1p	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 ↔ 𝐹 = ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) )
55	45 8 51 54	syl3anc	⊢ ( 𝜑 → ( 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 ↔ 𝐹 = ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) )
56	43 55	mpbid	⊢ ( 𝜑 → 𝐹 = ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) )
57	56	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) = ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) )
58	53 1 2 49	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 )
59	45 8 51 58	syl3anc	⊢ ( 𝜑 → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 )
60	1 2 46	mon1pcl	⊢ ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) → 𝐺 ∈ 𝐵 )
61	48 60	syl	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
62		eqid	⊢ ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) = ( .r ‘ ( 𝑅 ↑s 𝐾 ) )
63	2 52 62	rhmmul	⊢ ( ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) ∧ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝐺 ) ) )
64	26 59 61 63	syl3anc	⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝐺 ) ) )
65	28 59	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
66	28 61	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
67		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
68	18 19 7 21 65 66 67 62	pwsmulrval	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝐺 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) )
69	57 64 68	3eqtrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) = ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) )
70	69	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑥 ) )
71	70	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑥 ) )
72	18 9 19 7 21 65	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) : 𝐾 ⟶ 𝐾 )
73	72	ffnd	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) Fn 𝐾 )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) Fn 𝐾 )
75	18 9 19 7 21 66	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) : 𝐾 ⟶ 𝐾 )
76	75	ffnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) Fn 𝐾 )
77	76	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( 𝑂 ‘ 𝐺 ) Fn 𝐾 )
78	20	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝐾 ∈ V )
79		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ 𝐾 )
80		fnfvof	⊢ ( ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) Fn 𝐾 ∧ ( 𝑂 ‘ 𝐺 ) Fn 𝐾 ) ∧ ( 𝐾 ∈ V ∧ 𝑥 ∈ 𝐾 ) ) → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) )
81	74 77 78 79 80	syl22anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∘f ( .r ‘ 𝑅 ) ( 𝑂 ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) )
82	71 81	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) )
83	82	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 𝑊 ↔ ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) = 𝑊 ) )
84	7 36	syl	⊢ ( 𝜑 → 𝑅 ∈ Domn )
85	84	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑅 ∈ Domn )
86	72	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ∈ 𝐾 )
87	75	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐾 )
88	9 67 5	domneq0	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐾 ) → ( ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) = 𝑊 ↔ ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ∨ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
89	85 86 87 88	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) ) = 𝑊 ↔ ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ∨ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
90	83 89	bitrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 𝑊 ↔ ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ∨ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
91	90	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 𝑊 ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ∨ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) ) )
92		andi	⊢ ( ( 𝑥 ∈ 𝐾 ∧ ( ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ∨ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) ↔ ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ) ∨ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
93	91 92	bitrdi	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 𝑊 ) ↔ ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ) ∨ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) ) )
94		fniniseg	⊢ ( ( 𝑂 ‘ 𝐹 ) Fn 𝐾 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 𝑊 ) ) )
95	31 94	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑥 ) = 𝑊 ) ) )
96		elun	⊢ ( 𝑥 ∈ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ↔ ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∨ 𝑥 ∈ { 𝑇 } ) )
97		fniniseg	⊢ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) Fn 𝐾 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ) ) )
98	73 97	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ) ) )
99	47	simp3d	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 𝑊 } ) = { 𝑇 } )
100	99	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 𝑊 } ) ↔ 𝑥 ∈ { 𝑇 } ) )
101		fniniseg	⊢ ( ( 𝑂 ‘ 𝐺 ) Fn 𝐾 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 𝑊 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
102	76 101	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 𝑊 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
103	100 102	bitr3d	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑇 } ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) )
104	98 103	orbi12d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∨ 𝑥 ∈ { 𝑇 } ) ↔ ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ) ∨ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) ) )
105	96 104	syl5bb	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ↔ ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ‘ 𝑥 ) = 𝑊 ) ∨ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 𝑊 ) ) ) )
106	93 95 105	3bitr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ 𝑥 ∈ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) )
107	106	eqrdv	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) = ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) )
108	107	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ) = ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) )
109		fvex	⊢ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ V
110	109	cnvex	⊢ ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ V
111	110	imaex	⊢ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ V
112	111	a1i	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ V )
113	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	fta1glem1	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) = 𝑁 )
114		fveq2	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
115	114	eqeq1d	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( ( 𝐷 ‘ 𝑔 ) = 𝑁 ↔ ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) = 𝑁 ) )
116		fveq2	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( 𝑂 ‘ 𝑔 ) = ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
117	116	cnveqd	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ◡ ( 𝑂 ‘ 𝑔 ) = ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
118	117	imaeq1d	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( ◡ ( 𝑂 ‘ 𝑔 ) “ { 𝑊 } ) = ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) )
119	118	fveq2d	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑔 ) “ { 𝑊 } ) ) = ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) )
120	119 114	breq12d	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑔 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑔 ) ↔ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) )
121	115 120	imbi12d	⊢ ( 𝑔 = ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) → ( ( ( 𝐷 ‘ 𝑔 ) = 𝑁 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑔 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑔 ) ) ↔ ( ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) = 𝑁 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) ) )
122	121 17 59	rspcdva	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) = 𝑁 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) )
123	113 122	mpd	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
124	123 113	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ≤ 𝑁 )
125		hashbnd	⊢ ( ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ V ∧ 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ≤ 𝑁 ) → ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ Fin )
126	112 14 124 125	syl3anc	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ Fin )
127		snfi	⊢ { 𝑇 } ∈ Fin
128		unfi	⊢ ( ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ Fin ∧ { 𝑇 } ∈ Fin ) → ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ∈ Fin )
129	126 127 128	sylancl	⊢ ( 𝜑 → ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ∈ Fin )
130		hashcl	⊢ ( ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ∈ Fin → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ∈ ℕ0 )
131	129 130	syl	⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ∈ ℕ0 )
132	131	nn0red	⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ∈ ℝ )
133		hashcl	⊢ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ Fin → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ∈ ℕ0 )
134	126 133	syl	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ∈ ℕ0 )
135	134	nn0red	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ∈ ℝ )
136		peano2re	⊢ ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) ∈ ℝ → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + 1 ) ∈ ℝ )
137	135 136	syl	⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + 1 ) ∈ ℝ )
138		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
139	14 138	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
140	15 139	eqeltrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
141	140	nn0red	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
142		hashun2	⊢ ( ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∈ Fin ∧ { 𝑇 } ∈ Fin ) → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ≤ ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + ( ♯ ‘ { 𝑇 } ) ) )
143	126 127 142	sylancl	⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ≤ ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + ( ♯ ‘ { 𝑇 } ) ) )
144		hashsng	⊢ ( 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) → ( ♯ ‘ { 𝑇 } ) = 1 )
145	16 144	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝑇 } ) = 1 )
146	145	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + ( ♯ ‘ { 𝑇 } ) ) = ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + 1 ) )
147	143 146	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ≤ ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + 1 ) )
148	14	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
149		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
150	135 148 149 124	leadd1dd	⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + 1 ) ≤ ( 𝑁 + 1 ) )
151	150 15	breqtrrd	⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ) + 1 ) ≤ ( 𝐷 ‘ 𝐹 ) )
152	132 137 141 147 151	letrd	⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝑂 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) “ { 𝑊 } ) ∪ { 𝑇 } ) ) ≤ ( 𝐷 ‘ 𝐹 ) )
153	108 152	eqbrtrd	⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝐹 ) )