Metamath Proof Explorer

Theorem ig1peu

Description: There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1peu.p 
|- P = ( Poly1 ` R )
ig1peu.u 
|- U = ( LIdeal ` P )
ig1peu.z 
|- .0. = ( 0g ` P )
ig1peu.m 
|- M = ( Monic1p ` R )
ig1peu.d 
|- D = ( deg1 ` R )
Assertion ig1peu 
|- ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E! g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )

Proof

Step Hyp Ref Expression
1 ig1peu.p 
 |-  P = ( Poly1 ` R )
2 ig1peu.u 
 |-  U = ( LIdeal ` P )
3 ig1peu.z 
 |-  .0. = ( 0g ` P )
4 ig1peu.m 
 |-  M = ( Monic1p ` R )
5 ig1peu.d 
 |-  D = ( deg1 ` R )
6 eqid 
 |-  ( Base ` P ) = ( Base ` P )
7 6 2 lidlss 
 |-  ( I e. U -> I C_ ( Base ` P ) )
8 7 3ad2ant2 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> I C_ ( Base ` P ) )
9 8 ssdifd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( I \ { .0. } ) C_ ( ( Base ` P ) \ { .0. } ) )
10 imass2 
 |-  ( ( I \ { .0. } ) C_ ( ( Base ` P ) \ { .0. } ) -> ( D " ( I \ { .0. } ) ) C_ ( D " ( ( Base ` P ) \ { .0. } ) ) )
11 9 10 syl 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( D " ( I \ { .0. } ) ) C_ ( D " ( ( Base ` P ) \ { .0. } ) ) )
12 drngring 
 |-  ( R e. DivRing -> R e. Ring )
13 12 3ad2ant1 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> R e. Ring )
14 5 1 3 6 deg1n0ima 
 |-  ( R e. Ring -> ( D " ( ( Base ` P ) \ { .0. } ) ) C_ NN0 )
15 13 14 syl 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( D " ( ( Base ` P ) \ { .0. } ) ) C_ NN0 )
16 11 15 sstrd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( D " ( I \ { .0. } ) ) C_ NN0 )
17 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
18 16 17 sseqtrdi 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( D " ( I \ { .0. } ) ) C_ ( ZZ>= ` 0 ) )
19 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
20 13 19 syl 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> P e. Ring )
21 simp2 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> I e. U )
22 2 3 lidl0cl 
 |-  ( ( P e. Ring /\ I e. U ) -> .0. e. I )
23 20 21 22 syl2anc 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> .0. e. I )
24 23 snssd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> { .0. } C_ I )
25 simp3 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> I =/= { .0. } )
26 25 necomd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> { .0. } =/= I )
27 pssdifn0 
 |-  ( ( { .0. } C_ I /\ { .0. } =/= I ) -> ( I \ { .0. } ) =/= (/) )
28 24 26 27 syl2anc 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( I \ { .0. } ) =/= (/) )
29 5 1 6 deg1xrf 
 |-  D : ( Base ` P ) --> RR*
30 ffn 
 |-  ( D : ( Base ` P ) --> RR* -> D Fn ( Base ` P ) )
31 29 30 ax-mp 
 |-  D Fn ( Base ` P )
32 31 a1i 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> D Fn ( Base ` P ) )
33 8 ssdifssd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( I \ { .0. } ) C_ ( Base ` P ) )
34 fnimaeq0 
 |-  ( ( D Fn ( Base ` P ) /\ ( I \ { .0. } ) C_ ( Base ` P ) ) -> ( ( D " ( I \ { .0. } ) ) = (/) <-> ( I \ { .0. } ) = (/) ) )
35 32 33 34 syl2anc 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( ( D " ( I \ { .0. } ) ) = (/) <-> ( I \ { .0. } ) = (/) ) )
36 35 necon3bid 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( ( D " ( I \ { .0. } ) ) =/= (/) <-> ( I \ { .0. } ) =/= (/) ) )
37 28 36 mpbird 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( D " ( I \ { .0. } ) ) =/= (/) )
38 infssuzcl 
 |-  ( ( ( D " ( I \ { .0. } ) ) C_ ( ZZ>= ` 0 ) /\ ( D " ( I \ { .0. } ) ) =/= (/) ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) e. ( D " ( I \ { .0. } ) ) )
39 18 37 38 syl2anc 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) e. ( D " ( I \ { .0. } ) ) )
40 32 33 fvelimabd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( inf ( ( D " ( I \ { .0. } ) ) , RR , < ) e. ( D " ( I \ { .0. } ) ) <-> E. h e. ( I \ { .0. } ) ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
41 39 40 mpbid 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E. h e. ( I \ { .0. } ) ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
42 20 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> P e. Ring )
43 simpl2 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> I e. U )
44 13 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> R e. Ring )
45 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
46 eqid 
 |-  ( Base ` R ) = ( Base ` R )
47 1 45 46 6 ply1sclf 
 |-  ( R e. Ring -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
48 44 47 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
49 simpl1 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> R e. DivRing )
50 33 sselda 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> h e. ( Base ` P ) )
51 eldifsni 
 |-  ( h e. ( I \ { .0. } ) -> h =/= .0. )
52 51 adantl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> h =/= .0. )
53 eqid 
 |-  ( Unic1p ` R ) = ( Unic1p ` R )
54 1 6 3 53 drnguc1p 
 |-  ( ( R e. DivRing /\ h e. ( Base ` P ) /\ h =/= .0. ) -> h e. ( Unic1p ` R ) )
55 49 50 52 54 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> h e. ( Unic1p ` R ) )
56 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
57 5 56 53 uc1pldg 
 |-  ( h e. ( Unic1p ` R ) -> ( ( coe1 ` h ) ` ( D ` h ) ) e. ( Unit ` R ) )
58 55 57 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( coe1 ` h ) ` ( D ` h ) ) e. ( Unit ` R ) )
59 eqid 
 |-  ( invr ` R ) = ( invr ` R )
60 56 59 unitinvcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` h ) ` ( D ` h ) ) e. ( Unit ` R ) ) -> ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( Unit ` R ) )
61 44 58 60 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( Unit ` R ) )
62 46 56 unitcl 
 |-  ( ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( Unit ` R ) -> ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( Base ` R ) )
63 61 62 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( Base ` R ) )
64 48 63 ffvelrnd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) e. ( Base ` P ) )
65 eldifi 
 |-  ( h e. ( I \ { .0. } ) -> h e. I )
66 65 adantl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> h e. I )
67 eqid 
 |-  ( .r ` P ) = ( .r ` P )
68 2 6 67 lidlmcl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) e. ( Base ` P ) /\ h e. I ) ) -> ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) e. I )
69 42 43 64 66 68 syl22anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) e. I )
70 53 4 1 67 45 5 59 uc1pmon1p 
 |-  ( ( R e. Ring /\ h e. ( Unic1p ` R ) ) -> ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) e. M )
71 44 55 70 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) e. M )
72 69 71 elind 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) e. ( I i^i M ) )
73 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
74 73 56 unitrrg 
 |-  ( R e. Ring -> ( Unit ` R ) C_ ( RLReg ` R ) )
75 44 74 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( Unit ` R ) C_ ( RLReg ` R ) )
76 75 61 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( RLReg ` R ) )
77 5 1 73 6 67 45 deg1mul3 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) e. ( RLReg ` R ) /\ h e. ( Base ` P ) ) -> ( D ` ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) ) = ( D ` h ) )
78 44 76 50 77 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( D ` ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) ) = ( D ` h ) )
79 fveqeq2 
 |-  ( g = ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) -> ( ( D ` g ) = ( D ` h ) <-> ( D ` ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) ) = ( D ` h ) ) )
80 79 rspcev 
 |-  ( ( ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) e. ( I i^i M ) /\ ( D ` ( ( ( algSc ` P ) ` ( ( invr ` R ) ` ( ( coe1 ` h ) ` ( D ` h ) ) ) ) ( .r ` P ) h ) ) = ( D ` h ) ) -> E. g e. ( I i^i M ) ( D ` g ) = ( D ` h ) )
81 72 78 80 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> E. g e. ( I i^i M ) ( D ` g ) = ( D ` h ) )
82 eqeq2 
 |-  ( ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) -> ( ( D ` g ) = ( D ` h ) <-> ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
83 82 rexbidv 
 |-  ( ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) -> ( E. g e. ( I i^i M ) ( D ` g ) = ( D ` h ) <-> E. g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
84 81 83 syl5ibcom 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ h e. ( I \ { .0. } ) ) -> ( ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) -> E. g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
85 84 rexlimdva 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( E. h e. ( I \ { .0. } ) ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) -> E. g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
86 41 85 mpd 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E. g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
87 eqid 
 |-  ( -g ` P ) = ( -g ` P )
88 13 ad2antrr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) -> R e. Ring )
89 simprl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> g e. ( I i^i M ) )
90 89 elin2d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> g e. M )
91 90 adantr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) -> g e. M )
92 simprl 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) -> ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
93 simprr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> h e. ( I i^i M ) )
94 93 elin2d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> h e. M )
95 94 adantr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) -> h e. M )
96 simprr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) -> ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
97 5 4 1 87 88 91 92 95 96 deg1submon1p 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) -> ( D ` ( g ( -g ` P ) h ) ) < inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
98 97 ex 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) -> ( D ` ( g ( -g ` P ) h ) ) < inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
99 18 ad2antrr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> ( D " ( I \ { .0. } ) ) C_ ( ZZ>= ` 0 ) )
100 31 a1i 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> D Fn ( Base ` P ) )
101 33 ad2antrr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> ( I \ { .0. } ) C_ ( Base ` P ) )
102 20 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> P e. Ring )
103 simpl2 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> I e. U )
104 89 elin1d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> g e. I )
105 93 elin1d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> h e. I )
106 2 87 lidlsubcl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( g e. I /\ h e. I ) ) -> ( g ( -g ` P ) h ) e. I )
107 102 103 104 105 106 syl22anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( g ( -g ` P ) h ) e. I )
108 107 adantr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> ( g ( -g ` P ) h ) e. I )
109 simpr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> ( g ( -g ` P ) h ) =/= .0. )
110 eldifsn 
 |-  ( ( g ( -g ` P ) h ) e. ( I \ { .0. } ) <-> ( ( g ( -g ` P ) h ) e. I /\ ( g ( -g ` P ) h ) =/= .0. ) )
111 108 109 110 sylanbrc 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> ( g ( -g ` P ) h ) e. ( I \ { .0. } ) )
112 fnfvima 
 |-  ( ( D Fn ( Base ` P ) /\ ( I \ { .0. } ) C_ ( Base ` P ) /\ ( g ( -g ` P ) h ) e. ( I \ { .0. } ) ) -> ( D ` ( g ( -g ` P ) h ) ) e. ( D " ( I \ { .0. } ) ) )
113 100 101 111 112 syl3anc 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> ( D ` ( g ( -g ` P ) h ) ) e. ( D " ( I \ { .0. } ) ) )
114 infssuzle 
 |-  ( ( ( D " ( I \ { .0. } ) ) C_ ( ZZ>= ` 0 ) /\ ( D ` ( g ( -g ` P ) h ) ) e. ( D " ( I \ { .0. } ) ) ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <_ ( D ` ( g ( -g ` P ) h ) ) )
115 99 113 114 syl2anc 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) /\ ( g ( -g ` P ) h ) =/= .0. ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <_ ( D ` ( g ( -g ` P ) h ) ) )
116 115 ex 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( g ( -g ` P ) h ) =/= .0. -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <_ ( D ` ( g ( -g ` P ) h ) ) ) )
117 imassrn 
 |-  ( D " ( I \ { .0. } ) ) C_ ran D
118 frn 
 |-  ( D : ( Base ` P ) --> RR* -> ran D C_ RR* )
119 29 118 ax-mp 
 |-  ran D C_ RR*
120 117 119 sstri 
 |-  ( D " ( I \ { .0. } ) ) C_ RR*
121 120 39 sseldi 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) e. RR* )
122 121 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) e. RR* )
123 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
124 20 123 syl 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> P e. Grp )
125 124 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> P e. Grp )
126 inss1 
 |-  ( I i^i M ) C_ I
127 126 8 sstrid 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( I i^i M ) C_ ( Base ` P ) )
128 127 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( I i^i M ) C_ ( Base ` P ) )
129 128 89 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> g e. ( Base ` P ) )
130 128 93 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> h e. ( Base ` P ) )
131 6 87 grpsubcl 
 |-  ( ( P e. Grp /\ g e. ( Base ` P ) /\ h e. ( Base ` P ) ) -> ( g ( -g ` P ) h ) e. ( Base ` P ) )
132 125 129 130 131 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( g ( -g ` P ) h ) e. ( Base ` P ) )
133 5 1 6 deg1xrcl 
 |-  ( ( g ( -g ` P ) h ) e. ( Base ` P ) -> ( D ` ( g ( -g ` P ) h ) ) e. RR* )
134 132 133 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( D ` ( g ( -g ` P ) h ) ) e. RR* )
135 122 134 xrlenltd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <_ ( D ` ( g ( -g ` P ) h ) ) <-> -. ( D ` ( g ( -g ` P ) h ) ) < inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
136 116 135 sylibd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( g ( -g ` P ) h ) =/= .0. -> -. ( D ` ( g ( -g ` P ) h ) ) < inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
137 136 necon4ad 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( D ` ( g ( -g ` P ) h ) ) < inf ( ( D " ( I \ { .0. } ) ) , RR , < ) -> ( g ( -g ` P ) h ) = .0. ) )
138 98 137 syld 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) -> ( g ( -g ` P ) h ) = .0. ) )
139 6 3 87 grpsubeq0 
 |-  ( ( P e. Grp /\ g e. ( Base ` P ) /\ h e. ( Base ` P ) ) -> ( ( g ( -g ` P ) h ) = .0. <-> g = h ) )
140 125 129 130 139 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( g ( -g ` P ) h ) = .0. <-> g = h ) )
141 138 140 sylibd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) /\ ( g e. ( I i^i M ) /\ h e. ( I i^i M ) ) ) -> ( ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) -> g = h ) )
142 141 ralrimivva 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> A. g e. ( I i^i M ) A. h e. ( I i^i M ) ( ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) -> g = h ) )
143 fveqeq2 
 |-  ( g = h -> ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <-> ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
144 143 reu4 
 |-  ( E! g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <-> ( E. g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ A. g e. ( I i^i M ) A. h e. ( I i^i M ) ( ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) /\ ( D ` h ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) -> g = h ) ) )
145 86 142 144 sylanbrc 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E! g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )