Metamath Proof Explorer

Theorem pzriprnglem12

Description: Lemma 12 for pzriprng : Q has a ring unity. (Contributed by AV, 23-Mar-2025)

Ref Expression
Hypotheses pzriprng.r 
|- R = ( ZZring Xs. ZZring )
pzriprng.i 
|- I = ( ZZ X. { 0 } )
pzriprng.j 
|- J = ( R |`s I )
pzriprng.1 
|- .1. = ( 1r ` J )
pzriprng.g 
|- .~ = ( R ~QG I )
pzriprng.q 
|- Q = ( R /s .~ )
Assertion pzriprnglem12 
|- ( X e. ( Base ` Q ) -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) )

Proof

Step Hyp Ref Expression
1 pzriprng.r 
 |-  R = ( ZZring Xs. ZZring )
2 pzriprng.i 
 |-  I = ( ZZ X. { 0 } )
3 pzriprng.j 
 |-  J = ( R |`s I )
4 pzriprng.1 
 |-  .1. = ( 1r ` J )
5 pzriprng.g 
 |-  .~ = ( R ~QG I )
6 pzriprng.q 
 |-  Q = ( R /s .~ )
7 1 2 3 4 5 6 pzriprnglem11 
 |-  ( Base ` Q ) = U_ y e. ZZ { ( ZZ X. { y } ) }
8 7 eleq2i 
 |-  ( X e. ( Base ` Q ) <-> X e. U_ y e. ZZ { ( ZZ X. { y } ) } )
9 eliun 
 |-  ( X e. U_ y e. ZZ { ( ZZ X. { y } ) } <-> E. y e. ZZ X e. { ( ZZ X. { y } ) } )
10 8 9 bitri 
 |-  ( X e. ( Base ` Q ) <-> E. y e. ZZ X e. { ( ZZ X. { y } ) } )
11 elsni 
 |-  ( X e. { ( ZZ X. { y } ) } -> X = ( ZZ X. { y } ) )
12 1z 
 |-  1 e. ZZ
13 1 2 3 4 5 pzriprnglem10 
 |-  ( ( 1 e. ZZ /\ y e. ZZ ) -> [ <. 1 , y >. ] .~ = ( ZZ X. { y } ) )
14 12 13 mpan 
 |-  ( y e. ZZ -> [ <. 1 , y >. ] .~ = ( ZZ X. { y } ) )
15 14 eqcomd 
 |-  ( y e. ZZ -> ( ZZ X. { y } ) = [ <. 1 , y >. ] .~ )
16 15 eqeq2d 
 |-  ( y e. ZZ -> ( X = ( ZZ X. { y } ) <-> X = [ <. 1 , y >. ] .~ ) )
17 1 pzriprnglem1 
 |-  R e. Rng
18 17 a1i 
 |-  ( y e. ZZ -> R e. Rng )
19 1 2 3 pzriprnglem8 
 |-  I e. ( 2Ideal ` R )
20 19 a1i 
 |-  ( y e. ZZ -> I e. ( 2Ideal ` R ) )
21 1 2 pzriprnglem4 
 |-  I e. ( SubGrp ` R )
22 21 a1i 
 |-  ( y e. ZZ -> I e. ( SubGrp ` R ) )
23 12 a1i 
 |-  ( y e. ZZ -> 1 e. ZZ )
24 23 23 opelxpd 
 |-  ( y e. ZZ -> <. 1 , 1 >. e. ( ZZ X. ZZ ) )
25 id 
 |-  ( y e. ZZ -> y e. ZZ )
26 23 25 opelxpd 
 |-  ( y e. ZZ -> <. 1 , y >. e. ( ZZ X. ZZ ) )
27 1 pzriprnglem2 
 |-  ( Base ` R ) = ( ZZ X. ZZ )
28 27 eqcomi 
 |-  ( ZZ X. ZZ ) = ( Base ` R )
29 eqid 
 |-  ( .r ` R ) = ( .r ` R )
30 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
31 5 6 28 29 30 qusmulrng 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) /\ ( <. 1 , 1 >. e. ( ZZ X. ZZ ) /\ <. 1 , y >. e. ( ZZ X. ZZ ) ) ) -> ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) = [ ( <. 1 , 1 >. ( .r ` R ) <. 1 , y >. ) ] .~ )
32 18 20 22 24 26 31 syl32anc 
 |-  ( y e. ZZ -> ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) = [ ( <. 1 , 1 >. ( .r ` R ) <. 1 , y >. ) ] .~ )
33 zringbas 
 |-  ZZ = ( Base ` ZZring )
34 zringring 
 |-  ZZring e. Ring
35 34 a1i 
 |-  ( y e. ZZ -> ZZring e. Ring )
36 23 23 zmulcld 
 |-  ( y e. ZZ -> ( 1 x. 1 ) e. ZZ )
37 23 25 zmulcld 
 |-  ( y e. ZZ -> ( 1 x. y ) e. ZZ )
38 zringmulr 
 |-  x. = ( .r ` ZZring )
39 1 33 33 35 35 23 23 23 25 36 37 38 38 29 xpsmul 
 |-  ( y e. ZZ -> ( <. 1 , 1 >. ( .r ` R ) <. 1 , y >. ) = <. ( 1 x. 1 ) , ( 1 x. y ) >. )
40 1cnd 
 |-  ( y e. ZZ -> 1 e. CC )
41 40 mulridd 
 |-  ( y e. ZZ -> ( 1 x. 1 ) = 1 )
42 zcn 
 |-  ( y e. ZZ -> y e. CC )
43 42 mullidd 
 |-  ( y e. ZZ -> ( 1 x. y ) = y )
44 41 43 opeq12d 
 |-  ( y e. ZZ -> <. ( 1 x. 1 ) , ( 1 x. y ) >. = <. 1 , y >. )
45 39 44 eqtrd 
 |-  ( y e. ZZ -> ( <. 1 , 1 >. ( .r ` R ) <. 1 , y >. ) = <. 1 , y >. )
46 45 eceq1d 
 |-  ( y e. ZZ -> [ ( <. 1 , 1 >. ( .r ` R ) <. 1 , y >. ) ] .~ = [ <. 1 , y >. ] .~ )
47 32 46 eqtrd 
 |-  ( y e. ZZ -> ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) = [ <. 1 , y >. ] .~ )
48 5 6 28 29 30 qusmulrng 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) /\ ( <. 1 , y >. e. ( ZZ X. ZZ ) /\ <. 1 , 1 >. e. ( ZZ X. ZZ ) ) ) -> ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) = [ ( <. 1 , y >. ( .r ` R ) <. 1 , 1 >. ) ] .~ )
49 18 20 22 26 24 48 syl32anc 
 |-  ( y e. ZZ -> ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) = [ ( <. 1 , y >. ( .r ` R ) <. 1 , 1 >. ) ] .~ )
50 25 23 zmulcld 
 |-  ( y e. ZZ -> ( y x. 1 ) e. ZZ )
51 1 33 33 35 35 23 25 23 23 36 50 38 38 29 xpsmul 
 |-  ( y e. ZZ -> ( <. 1 , y >. ( .r ` R ) <. 1 , 1 >. ) = <. ( 1 x. 1 ) , ( y x. 1 ) >. )
52 42 mulridd 
 |-  ( y e. ZZ -> ( y x. 1 ) = y )
53 41 52 opeq12d 
 |-  ( y e. ZZ -> <. ( 1 x. 1 ) , ( y x. 1 ) >. = <. 1 , y >. )
54 51 53 eqtrd 
 |-  ( y e. ZZ -> ( <. 1 , y >. ( .r ` R ) <. 1 , 1 >. ) = <. 1 , y >. )
55 54 eceq1d 
 |-  ( y e. ZZ -> [ ( <. 1 , y >. ( .r ` R ) <. 1 , 1 >. ) ] .~ = [ <. 1 , y >. ] .~ )
56 49 55 eqtrd 
 |-  ( y e. ZZ -> ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) = [ <. 1 , y >. ] .~ )
57 47 56 jca 
 |-  ( y e. ZZ -> ( ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) = [ <. 1 , y >. ] .~ /\ ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) = [ <. 1 , y >. ] .~ ) )
58 1 2 3 4 5 pzriprnglem10 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ ) -> [ <. 1 , 1 >. ] .~ = ( ZZ X. { 1 } ) )
59 12 12 58 mp2an 
 |-  [ <. 1 , 1 >. ] .~ = ( ZZ X. { 1 } )
60 59 eqcomi 
 |-  ( ZZ X. { 1 } ) = [ <. 1 , 1 >. ] .~
61 60 a1i 
 |-  ( X = [ <. 1 , y >. ] .~ -> ( ZZ X. { 1 } ) = [ <. 1 , 1 >. ] .~ )
62 id 
 |-  ( X = [ <. 1 , y >. ] .~ -> X = [ <. 1 , y >. ] .~ )
63 61 62 oveq12d 
 |-  ( X = [ <. 1 , y >. ] .~ -> ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) )
64 63 62 eqeq12d 
 |-  ( X = [ <. 1 , y >. ] .~ -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X <-> ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) = [ <. 1 , y >. ] .~ ) )
65 62 61 oveq12d 
 |-  ( X = [ <. 1 , y >. ] .~ -> ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) )
66 65 62 eqeq12d 
 |-  ( X = [ <. 1 , y >. ] .~ -> ( ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X <-> ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) = [ <. 1 , y >. ] .~ ) )
67 64 66 anbi12d 
 |-  ( X = [ <. 1 , y >. ] .~ -> ( ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) <-> ( ( [ <. 1 , 1 >. ] .~ ( .r ` Q ) [ <. 1 , y >. ] .~ ) = [ <. 1 , y >. ] .~ /\ ( [ <. 1 , y >. ] .~ ( .r ` Q ) [ <. 1 , 1 >. ] .~ ) = [ <. 1 , y >. ] .~ ) ) )
68 57 67 syl5ibrcom 
 |-  ( y e. ZZ -> ( X = [ <. 1 , y >. ] .~ -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) ) )
69 16 68 sylbid 
 |-  ( y e. ZZ -> ( X = ( ZZ X. { y } ) -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) ) )
70 11 69 syl5 
 |-  ( y e. ZZ -> ( X e. { ( ZZ X. { y } ) } -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) ) )
71 70 rexlimiv 
 |-  ( E. y e. ZZ X e. { ( ZZ X. { y } ) } -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) )
72 10 71 sylbi 
 |-  ( X e. ( Base ` Q ) -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) X ) = X /\ ( X ( .r ` Q ) ( ZZ X. { 1 } ) ) = X ) )