Metamath Proof Explorer

Theorem minplyirredlem

Description: Lemma for minplyirred . (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
minplyirred.1 ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
minplyirred.2 ⊢ 𝑍 = ( 0g ‘ 𝑃 )
minplyirred.3 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )
minplyirredlem.1 ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝑃 ) )
minplyirredlem.2 ⊢ ( 𝜑 → 𝐻 ∈ ( Base ‘ 𝑃 ) )
minplyirredlem.3 ⊢ ( 𝜑 → ( 𝐺 ( .r ‘ 𝑃 ) 𝐻 ) = ( 𝑀 ‘ 𝐴 ) )
minplyirredlem.4 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) )
minplyirredlem.5 ⊢ ( 𝜑 → 𝐺 ≠ 𝑍 )
minplyirredlem.6 ⊢ ( 𝜑 → 𝐻 ≠ 𝑍 )
Assertion minplyirredlem ( 𝜑 → 𝐻 ∈ ( Unit ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
2 ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
3 ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
4 ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
5 ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
6 ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 minplyirred.1 ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
8 minplyirred.2 ⊢ 𝑍 = ( 0g ‘ 𝑃 )
9 minplyirred.3 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )
10 minplyirredlem.1 ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝑃 ) )
11 minplyirredlem.2 ⊢ ( 𝜑 → 𝐻 ∈ ( Base ‘ 𝑃 ) )
12 minplyirredlem.3 ⊢ ( 𝜑 → ( 𝐺 ( .r ‘ 𝑃 ) 𝐻 ) = ( 𝑀 ‘ 𝐴 ) )
13 minplyirredlem.4 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) )
14 minplyirredlem.5 ⊢ ( 𝜑 → 𝐺 ≠ 𝑍 )
15 minplyirredlem.6 ⊢ ( 𝜑 → 𝐻 ≠ 𝑍 )
16 eqid ⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
17 16 sdrgdrng ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
18 5 17 syl ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
19 18 drngringd ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Ring )
20 eqid ⊢ ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) = ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) )
21 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
22 20 2 8 21 deg1nn0cl ⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ Ring ∧ 𝐺 ∈ ( Base ‘ 𝑃 ) ∧ 𝐺 ≠ 𝑍 ) → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ∈ ℕ0 )
23 19 10 14 22 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ∈ ℕ0 )
24 23 nn0red ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ∈ ℝ )
25 20 2 8 21 deg1nn0cl ⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ Ring ∧ 𝐻 ∈ ( Base ‘ 𝑃 ) ∧ 𝐻 ≠ 𝑍 ) → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ∈ ℕ0 )
26 19 11 15 25 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ∈ ℕ0 )
27 26 nn0red ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ∈ ℝ )
28 eqid ⊢ ( RLReg ‘ ( 𝐸 ↾s 𝐹 ) ) = ( RLReg ‘ ( 𝐸 ↾s 𝐹 ) )
29 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
30 fldsdrgfld ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ) → ( 𝐸 ↾s 𝐹 ) ∈ Field )
31 4 5 30 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Field )
32 fldidom ⊢ ( ( 𝐸 ↾s 𝐹 ) ∈ Field → ( 𝐸 ↾s 𝐹 ) ∈ IDomn )
33 31 32 syl ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ IDomn )
34 33 idomdomd ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Domn )
35 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
36 20 2 8 21 28 35 deg1ldgdomn ⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ Domn ∧ 𝐺 ∈ ( Base ‘ 𝑃 ) ∧ 𝐺 ≠ 𝑍 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ) ∈ ( RLReg ‘ ( 𝐸 ↾s 𝐹 ) ) )
37 34 10 14 36 syl3anc ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ) ∈ ( RLReg ‘ ( 𝐸 ↾s 𝐹 ) ) )
38 20 2 28 21 29 8 19 10 14 37 11 15 deg1mul2 ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ ( 𝐺 ( .r ‘ 𝑃 ) 𝐻 ) ) = ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) + ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ) )
39 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
40 eqid ⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) }
41 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
42 eqid ⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
43 1 2 3 4 5 6 39 40 41 42 7 minplyval ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) )
44 12 43 eqtrd ⊢ ( 𝜑 → ( 𝐺 ( .r ‘ 𝑃 ) 𝐻 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) )
45 44 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ ( 𝐺 ( .r ‘ 𝑃 ) 𝐻 ) ) = ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) ) )
46 4 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
47 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
48 5 47 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
49 1 2 3 46 48 6 39 40 ply1annidl ⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ∈ ( LIdeal ‘ 𝑃 ) )
50 fveq2 ⊢ ( 𝑞 = 𝐺 → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ 𝐺 ) )
51 50 fveq1d ⊢ ( 𝑞 = 𝐺 → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) )
52 51 eqeq1d ⊢ ( 𝑞 = 𝐺 → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) ↔ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) ) )
53 1 2 21 46 48 evls1dm ⊢ ( 𝜑 → dom 𝑂 = ( Base ‘ 𝑃 ) )
54 10 53 eleqtrrd ⊢ ( 𝜑 → 𝐺 ∈ dom 𝑂 )
55 52 54 13 elrabd ⊢ ( 𝜑 → 𝐺 ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } )
56 2 42 21 18 49 20 8 55 14 ig1pmindeg ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) ) ≤ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) )
57 45 56 eqbrtrd ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ ( 𝐺 ( .r ‘ 𝑃 ) 𝐻 ) ) ≤ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) )
58 38 57 eqbrtrrd ⊢ ( 𝜑 → ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) + ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ) ≤ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) )
59 leaddle0 ⊢ ( ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ∈ ℝ ∧ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ∈ ℝ ) → ( ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) + ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ) ≤ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ↔ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ≤ 0 ) )
60 59 biimpa ⊢ ( ( ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ∈ ℝ ∧ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ∈ ℝ ) ∧ ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) + ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ) ≤ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐺 ) ) → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ≤ 0 )
61 24 27 58 60 syl21anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ≤ 0 )
62 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
63 20 2 21 62 deg1le0 ⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ Ring ∧ 𝐻 ∈ ( Base ‘ 𝑃 ) ) → ( ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ≤ 0 ↔ 𝐻 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ) ) )
64 63 biimpa ⊢ ( ( ( ( 𝐸 ↾s 𝐹 ) ∈ Ring ∧ 𝐻 ∈ ( Base ‘ 𝑃 ) ) ∧ ( ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ 𝐻 ) ≤ 0 ) → 𝐻 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ) )
65 19 11 61 64 syl21anc ⊢ ( 𝜑 → 𝐻 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ) )
66 eqid ⊢ ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) = ( Base ‘ ( 𝐸 ↾s 𝐹 ) )
67 eqid ⊢ ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) )
68 0nn0 ⊢ 0 ∈ ℕ0
69 eqid ⊢ ( coe1 ‘ 𝐻 ) = ( coe1 ‘ 𝐻 )
70 69 21 2 66 coe1fvalcl ⊢ ( ( 𝐻 ∈ ( Base ‘ 𝑃 ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ∈ ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
71 11 68 70 sylancl ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ∈ ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
72 20 2 67 21 8 19 11 61 deg1le0eq0 ⊢ ( 𝜑 → ( 𝐻 = 𝑍 ↔ ( ( coe1 ‘ 𝐻 ) ‘ 0 ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
73 72 necon3bid ⊢ ( 𝜑 → ( 𝐻 ≠ 𝑍 ↔ ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ≠ ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
74 15 73 mpbid ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ≠ ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) )
75 2 62 66 67 31 71 74 ply1asclunit ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐻 ) ‘ 0 ) ) ∈ ( Unit ‘ 𝑃 ) )
76 65 75 eqeltrd ⊢ ( 𝜑 → 𝐻 ∈ ( Unit ‘ 𝑃 ) )