ig1pdvds

Description: The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	ig1pval.g	⊢ 𝐺 = ( idlGen_1p ‘ 𝑅 )
	ig1pcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
	ig1pdvds.d	⊢ ∥ = ( ∥_r ‘ 𝑃 )
Assertion	ig1pdvds	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ig1pval.g	⊢ 𝐺 = ( idlGen_1p ‘ 𝑅 )
3		ig1pcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
4		ig1pdvds.d	⊢ ∥ = ( ∥_r ‘ 𝑃 )
5		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
7	5 6	syl	⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ Ring )
8	7	3ad2ant1	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → 𝑃 ∈ Ring )
9		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10	9 3	lidlss	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
11	10	3ad2ant2	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
12	1 2 3	ig1pcl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
13	12	3adant3	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
14	11 13	sseldd	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Base ‘ 𝑃 ) )
15		eqid	⊢ ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝑃 )
16	9 4 15	dvdsr01	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∥ ( 0_g ‘ 𝑃 ) )
17	8 14 16	syl2anc	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ∥ ( 0_g ‘ 𝑃 ) )
18	17	adantr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 = { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∥ ( 0_g ‘ 𝑃 ) )
19		eleq2	⊢ ( 𝐼 = { ( 0_g ‘ 𝑃 ) } → ( 𝑋 ∈ 𝐼 ↔ 𝑋 ∈ { ( 0_g ‘ 𝑃 ) } ) )
20	19	biimpac	⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐼 = { ( 0_g ‘ 𝑃 ) } ) → 𝑋 ∈ { ( 0_g ‘ 𝑃 ) } )
21	20	3ad2antl3	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 = { ( 0_g ‘ 𝑃 ) } ) → 𝑋 ∈ { ( 0_g ‘ 𝑃 ) } )
22		elsni	⊢ ( 𝑋 ∈ { ( 0_g ‘ 𝑃 ) } → 𝑋 = ( 0_g ‘ 𝑃 ) )
23	21 22	syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 = { ( 0_g ‘ 𝑃 ) } ) → 𝑋 = ( 0_g ‘ 𝑃 ) )
24	18 23	breqtrrd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 = { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 )
25		simpl1	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝑅 ∈ DivRing )
26	25 5	syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝑅 ∈ Ring )
27		simpl2	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝐼 ∈ 𝑈 )
28	27 10	syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
29		simpl3	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝑋 ∈ 𝐼 )
30	28 29	sseldd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
31		simpr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } )
32		eqid	⊢ ( deg₁ ‘ 𝑅 ) = ( deg₁ ‘ 𝑅 )
33		eqid	⊢ ( Monic_1p ‘ 𝑅 ) = ( Monic_1p ‘ 𝑅 )
34	1 2 15 3 32 33	ig1pval3	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Monic_1p ‘ 𝑅 ) ∧ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ) )
35	25 27 31 34	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Monic_1p ‘ 𝑅 ) ∧ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ) )
36	35	simp2d	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Monic_1p ‘ 𝑅 ) )
37		eqid	⊢ ( Unic_1p ‘ 𝑅 ) = ( Unic_1p ‘ 𝑅 )
38	37 33	mon1puc1p	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Monic_1p ‘ 𝑅 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Unic_1p ‘ 𝑅 ) )
39	26 36 38	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Unic_1p ‘ 𝑅 ) )
40		eqid	⊢ ( rem_1p ‘ 𝑅 ) = ( rem_1p ‘ 𝑅 )
41	40 1 9 37 32	r1pdeglt	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unic_1p ‘ 𝑅 ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) < ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝐼 ) ) )
42	26 30 39 41	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) < ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝐼 ) ) )
43	35	simp3d	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) )
44	42 43	breqtrd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) < inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) )
45	32 1 9	deg1xrf	⊢ ( deg₁ ‘ 𝑅 ) : ( Base ‘ 𝑃 ) ⟶ ℝ^*
46	35	simp1d	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
47	28 46	sseldd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Base ‘ 𝑃 ) )
48		eqid	⊢ ( quot_1p ‘ 𝑅 ) = ( quot_1p ‘ 𝑅 )
49		eqid	⊢ ( ._r ‘ 𝑃 ) = ( ._r ‘ 𝑃 )
50		eqid	⊢ ( -_g ‘ 𝑃 ) = ( -_g ‘ 𝑃 )
51	40 1 9 48 49 50	r1pval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) = ( 𝑋 ( -_g ‘ 𝑃 ) ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ) )
52	30 47 51	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) = ( 𝑋 ( -_g ‘ 𝑃 ) ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ) )
53	26 6	syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → 𝑃 ∈ Ring )
54	48 1 9 37	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unic_1p ‘ 𝑅 ) ) → ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
55	26 30 39 54	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
56	3 9 49	lidlmcl	⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ) ) → ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐼 )
57	53 27 55 46 56	syl22anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐼 )
58	3 50	lidlsubcl	⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐼 ) ) → ( 𝑋 ( -_g ‘ 𝑃 ) ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ 𝐼 )
59	53 27 29 57 58	syl22anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝑋 ( -_g ‘ 𝑃 ) ( ( 𝑋 ( quot_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ( ._r ‘ 𝑃 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ 𝐼 )
60	52 59	eqeltrd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐼 )
61	28 60	sseldd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
62		ffvelrn	⊢ ( ( ( deg₁ ‘ 𝑅 ) : ( Base ‘ 𝑃 ) ⟶ ℝ^* ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑃 ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ ℝ^* )
63	45 61 62	sylancr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ ℝ^* )
64	28	ssdifd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ⊆ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) )
65		imass2	⊢ ( ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ⊆ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ( deg₁ ‘ 𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) ) )
66	64 65	syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ( deg₁ ‘ 𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) ) )
67	32 1 15 9	deg1n0ima	⊢ ( 𝑅 ∈ Ring → ( ( deg₁ ‘ 𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ℕ₀ )
68	26 67	syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ℕ₀ )
69		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
70	68 69	sseqtrdi	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ℤ_≥ ‘ 0 ) )
71	66 70	sstrd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ℤ_≥ ‘ 0 ) )
72		uzssz	⊢ ( ℤ_≥ ‘ 0 ) ⊆ ℤ
73		zssre	⊢ ℤ ⊆ ℝ
74		ressxr	⊢ ℝ ⊆ ℝ^*
75	73 74	sstri	⊢ ℤ ⊆ ℝ^*
76	72 75	sstri	⊢ ( ℤ_≥ ‘ 0 ) ⊆ ℝ^*
77	71 76	sstrdi	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ℝ^* )
78	3 15	lidl0cl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0_g ‘ 𝑃 ) ∈ 𝐼 )
79	53 27 78	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 0_g ‘ 𝑃 ) ∈ 𝐼 )
80	79	snssd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → { ( 0_g ‘ 𝑃 ) } ⊆ 𝐼 )
81	31	necomd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → { ( 0_g ‘ 𝑃 ) } ≠ 𝐼 )
82		pssdifn0	⊢ ( ( { ( 0_g ‘ 𝑃 ) } ⊆ 𝐼 ∧ { ( 0_g ‘ 𝑃 ) } ≠ 𝐼 ) → ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ≠ ∅ )
83	80 81 82	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ≠ ∅ )
84		ffn	⊢ ( ( deg₁ ‘ 𝑅 ) : ( Base ‘ 𝑃 ) ⟶ ℝ^* → ( deg₁ ‘ 𝑅 ) Fn ( Base ‘ 𝑃 ) )
85	45 84	ax-mp	⊢ ( deg₁ ‘ 𝑅 ) Fn ( Base ‘ 𝑃 )
86	28	ssdifssd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ⊆ ( Base ‘ 𝑃 ) )
87		fnimaeq0	⊢ ( ( ( deg₁ ‘ 𝑅 ) Fn ( Base ‘ 𝑃 ) ∧ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ⊆ ( Base ‘ 𝑃 ) ) → ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) = ∅ ↔ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) = ∅ ) )
88	85 86 87	sylancr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) = ∅ ↔ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) = ∅ ) )
89	88	necon3bid	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ≠ ∅ ↔ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ≠ ∅ ) )
90	83 89	mpbird	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ≠ ∅ )
91		infssuzcl	⊢ ( ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ℤ_≥ ‘ 0 ) ∧ ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ≠ ∅ ) → inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ∈ ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) )
92	71 90 91	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ∈ ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) )
93	77 92	sseldd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ∈ ℝ^* )
94		xrltnle	⊢ ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ ℝ^* ∧ inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ∈ ℝ^* ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) < inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ↔ ¬ inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ) )
95	63 93 94	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) < inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ↔ ¬ inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ) )
96	44 95	mpbid	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ¬ inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) )
97	71	adantr	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) → ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ℤ_≥ ‘ 0 ) )
98	60	adantr	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐼 )
99		simpr	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) )
100		eldifsn	⊢ ( ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ↔ ( ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐼 ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) )
101	98 99 100	sylanbrc	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) )
102		fnfvima	⊢ ( ( ( deg₁ ‘ 𝑅 ) Fn ( Base ‘ 𝑃 ) ∧ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ∈ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) )
103	85 86 101 102	mp3an2ani	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) )
104		infssuzle	⊢ ( ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ⊆ ( ℤ_≥ ‘ 0 ) ∧ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ∈ ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) ) → inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) )
105	97 103 104	syl2anc	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) ∧ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) ) → inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) )
106	105	ex	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ≠ ( 0_g ‘ 𝑃 ) → inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) ) )
107	106	necon1bd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ¬ inf ( ( ( deg₁ ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0_g ‘ 𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) = ( 0_g ‘ 𝑃 ) ) )
108	96 107	mpd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) = ( 0_g ‘ 𝑃 ) )
109	1 4 9 37 15 40	dvdsr1p	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unic_1p ‘ 𝑅 ) ) → ( ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 ↔ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) = ( 0_g ‘ 𝑃 ) ) )
110	26 30 39 109	syl3anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 ↔ ( 𝑋 ( rem_1p ‘ 𝑅 ) ( 𝐺 ‘ 𝐼 ) ) = ( 0_g ‘ 𝑃 ) ) )
111	108 110	mpbird	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐼 ≠ { ( 0_g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 )
112	24 111	pm2.61dane	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 )

Metamath Proof Explorer

Theorem ig1pdvds

Proof