Metamath Proof Explorer

Theorem ressply1mon1p

Description: The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025)

Ref Expression
Hypotheses ressply.1 
|- S = ( Poly1 ` R )
ressply.2 
|- H = ( R |`s T )
ressply.3 
|- U = ( Poly1 ` H )
ressply.4 
|- B = ( Base ` U )
ressply.5 
|- ( ph -> T e. ( SubRing ` R ) )
ressply1mon1p.m 
|- M = ( Monic1p ` R )
ressply1mon1p.n 
|- N = ( Monic1p ` H )
Assertion ressply1mon1p 
|- ( ph -> N = ( B i^i M ) )

Proof

Step Hyp Ref Expression
1 ressply.1 
 |-  S = ( Poly1 ` R )
2 ressply.2 
 |-  H = ( R |`s T )
3 ressply.3 
 |-  U = ( Poly1 ` H )
4 ressply.4 
 |-  B = ( Base ` U )
5 ressply.5 
 |-  ( ph -> T e. ( SubRing ` R ) )
6 ressply1mon1p.m 
 |-  M = ( Monic1p ` R )
7 ressply1mon1p.n 
 |-  N = ( Monic1p ` H )
8 eqid 
 |-  ( Base ` S ) = ( Base ` S )
9 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
10 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 1 8 9 10 6 11 ismon1p 
 |-  ( p e. M <-> ( p e. ( Base ` S ) /\ p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) )
13 12 anbi2i 
 |-  ( ( p e. B /\ p e. M ) <-> ( p e. B /\ ( p e. ( Base ` S ) /\ p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) )
14 eqid 
 |-  ( S |`s B ) = ( S |`s B )
15 1 2 3 4 5 14 ressply1bas 
 |-  ( ph -> B = ( Base ` ( S |`s B ) ) )
16 14 8 ressbasss 
 |-  ( Base ` ( S |`s B ) ) C_ ( Base ` S )
17 15 16 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` S ) )
18 17 sseld 
 |-  ( ph -> ( p e. B -> p e. ( Base ` S ) ) )
19 18 pm4.71d 
 |-  ( ph -> ( p e. B <-> ( p e. B /\ p e. ( Base ` S ) ) ) )
20 19 anbi1d 
 |-  ( ph -> ( ( p e. B /\ ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) <-> ( ( p e. B /\ p e. ( Base ` S ) ) /\ ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) ) )
21 13an22anass 
 |-  ( ( p e. B /\ ( p e. ( Base ` S ) /\ p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) <-> ( ( p e. B /\ p e. ( Base ` S ) ) /\ ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) )
22 20 21 bitr4di 
 |-  ( ph -> ( ( p e. B /\ ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) <-> ( p e. B /\ ( p e. ( Base ` S ) /\ p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) ) )
23 1 2 3 4 5 9 ressply10g 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
24 23 neeq2d 
 |-  ( ph -> ( p =/= ( 0g ` S ) <-> p =/= ( 0g ` U ) ) )
25 24 adantr 
 |-  ( ( ph /\ p e. B ) -> ( p =/= ( 0g ` S ) <-> p =/= ( 0g ` U ) ) )
26 simpr 
 |-  ( ( ph /\ p e. B ) -> p e. B )
27 5 adantr 
 |-  ( ( ph /\ p e. B ) -> T e. ( SubRing ` R ) )
28 2 10 3 4 26 27 ressdeg1 
 |-  ( ( ph /\ p e. B ) -> ( ( deg1 ` R ) ` p ) = ( ( deg1 ` H ) ` p ) )
29 28 fveq2d 
 |-  ( ( ph /\ p e. B ) -> ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) )
30 2 11 subrg1 
 |-  ( T e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` H ) )
31 5 30 syl 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` H ) )
32 31 adantr 
 |-  ( ( ph /\ p e. B ) -> ( 1r ` R ) = ( 1r ` H ) )
33 29 32 eqeq12d 
 |-  ( ( ph /\ p e. B ) -> ( ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) <-> ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) )
34 25 33 anbi12d 
 |-  ( ( ph /\ p e. B ) -> ( ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) <-> ( p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) ) )
35 34 pm5.32da 
 |-  ( ph -> ( ( p e. B /\ ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) <-> ( p e. B /\ ( p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) ) ) )
36 3anass 
 |-  ( ( p e. B /\ p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) <-> ( p e. B /\ ( p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) ) )
37 35 36 bitr4di 
 |-  ( ph -> ( ( p e. B /\ ( p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) <-> ( p e. B /\ p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) ) )
38 22 37 bitr3d 
 |-  ( ph -> ( ( p e. B /\ ( p e. ( Base ` S ) /\ p =/= ( 0g ` S ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) ) <-> ( p e. B /\ p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) ) )
39 13 38 bitr2id 
 |-  ( ph -> ( ( p e. B /\ p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) <-> ( p e. B /\ p e. M ) ) )
40 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
41 eqid 
 |-  ( deg1 ` H ) = ( deg1 ` H )
42 eqid 
 |-  ( 1r ` H ) = ( 1r ` H )
43 3 4 40 41 7 42 ismon1p 
 |-  ( p e. N <-> ( p e. B /\ p =/= ( 0g ` U ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` H ) ` p ) ) = ( 1r ` H ) ) )
44 elin 
 |-  ( p e. ( B i^i M ) <-> ( p e. B /\ p e. M ) )
45 39 43 44 3bitr4g 
 |-  ( ph -> ( p e. N <-> p e. ( B i^i M ) ) )
46 45 eqrdv 
 |-  ( ph -> N = ( B i^i M ) )