Metamath Proof Explorer

Theorem pzriprnglem4

Description: Lemma 4 for pzriprng : I is a subgroup of R . (Contributed by AV, 18-Mar-2025)

Ref Expression
Hypotheses pzriprng.r 
|- R = ( ZZring Xs. ZZring )
pzriprng.i 
|- I = ( ZZ X. { 0 } )
Assertion pzriprnglem4 
|- I e. ( SubGrp ` R )

Proof

Step Hyp Ref Expression
1 pzriprng.r 
 |-  R = ( ZZring Xs. ZZring )
2 pzriprng.i 
 |-  I = ( ZZ X. { 0 } )
3 0z 
 |-  0 e. ZZ
4 c0ex 
 |-  0 e. _V
5 4 snss 
 |-  ( 0 e. ZZ <-> { 0 } C_ ZZ )
6 3 5 mpbi 
 |-  { 0 } C_ ZZ
7 xpss2 
 |-  ( { 0 } C_ ZZ -> ( ZZ X. { 0 } ) C_ ( ZZ X. ZZ ) )
8 6 7 ax-mp 
 |-  ( ZZ X. { 0 } ) C_ ( ZZ X. ZZ )
9 1 pzriprnglem2 
 |-  ( Base ` R ) = ( ZZ X. ZZ )
10 8 2 9 3sstr4i 
 |-  I C_ ( Base ` R )
11 3 ne0ii 
 |-  ZZ =/= (/)
12 4 snnz 
 |-  { 0 } =/= (/)
13 11 12 pm3.2i 
 |-  ( ZZ =/= (/) /\ { 0 } =/= (/) )
14 xpnz 
 |-  ( ( ZZ =/= (/) /\ { 0 } =/= (/) ) <-> ( ZZ X. { 0 } ) =/= (/) )
15 13 14 mpbi 
 |-  ( ZZ X. { 0 } ) =/= (/)
16 2 15 eqnetri 
 |-  I =/= (/)
17 1 2 pzriprnglem3 
 |-  ( x e. I <-> E. a e. ZZ x = <. a , 0 >. )
18 1 2 pzriprnglem3 
 |-  ( y e. I <-> E. b e. ZZ y = <. b , 0 >. )
19 simpr 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> x = <. a , 0 >. )
20 19 adantr 
 |-  ( ( ( a e. ZZ /\ x = <. a , 0 >. ) /\ b e. ZZ ) -> x = <. a , 0 >. )
21 id 
 |-  ( y = <. b , 0 >. -> y = <. b , 0 >. )
22 20 21 oveqan12d 
 |-  ( ( ( ( a e. ZZ /\ x = <. a , 0 >. ) /\ b e. ZZ ) /\ y = <. b , 0 >. ) -> ( x ( +g ` R ) y ) = ( <. a , 0 >. ( +g ` R ) <. b , 0 >. ) )
23 zringbas 
 |-  ZZ = ( Base ` ZZring )
24 zringring 
 |-  ZZring e. Ring
25 24 a1i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ZZring e. Ring )
26 simpl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. ZZ )
27 3 a1i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> 0 e. ZZ )
28 simpr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
29 zaddcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
30 00id 
 |-  ( 0 + 0 ) = 0
31 30 3 eqeltri 
 |-  ( 0 + 0 ) e. ZZ
32 31 a1i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( 0 + 0 ) e. ZZ )
33 zringplusg 
 |-  + = ( +g ` ZZring )
34 eqid 
 |-  ( +g ` R ) = ( +g ` R )
35 1 23 23 25 25 26 27 28 27 29 32 33 33 34 xpsadd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( <. a , 0 >. ( +g ` R ) <. b , 0 >. ) = <. ( a + b ) , ( 0 + 0 ) >. )
36 4 snid 
 |-  0 e. { 0 }
37 30 36 eqeltri 
 |-  ( 0 + 0 ) e. { 0 }
38 2 eleq2i 
 |-  ( <. ( a + b ) , ( 0 + 0 ) >. e. I <-> <. ( a + b ) , ( 0 + 0 ) >. e. ( ZZ X. { 0 } ) )
39 opelxp 
 |-  ( <. ( a + b ) , ( 0 + 0 ) >. e. ( ZZ X. { 0 } ) <-> ( ( a + b ) e. ZZ /\ ( 0 + 0 ) e. { 0 } ) )
40 38 39 bitri 
 |-  ( <. ( a + b ) , ( 0 + 0 ) >. e. I <-> ( ( a + b ) e. ZZ /\ ( 0 + 0 ) e. { 0 } ) )
41 29 37 40 sylanblrc 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> <. ( a + b ) , ( 0 + 0 ) >. e. I )
42 35 41 eqeltrd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( <. a , 0 >. ( +g ` R ) <. b , 0 >. ) e. I )
43 42 ad4ant13 
 |-  ( ( ( ( a e. ZZ /\ x = <. a , 0 >. ) /\ b e. ZZ ) /\ y = <. b , 0 >. ) -> ( <. a , 0 >. ( +g ` R ) <. b , 0 >. ) e. I )
44 22 43 eqeltrd 
 |-  ( ( ( ( a e. ZZ /\ x = <. a , 0 >. ) /\ b e. ZZ ) /\ y = <. b , 0 >. ) -> ( x ( +g ` R ) y ) e. I )
45 44 rexlimdva2 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> ( E. b e. ZZ y = <. b , 0 >. -> ( x ( +g ` R ) y ) e. I ) )
46 18 45 biimtrid 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> ( y e. I -> ( x ( +g ` R ) y ) e. I ) )
47 46 ralrimiv 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> A. y e. I ( x ( +g ` R ) y ) e. I )
48 zringgrp 
 |-  ZZring e. Grp
49 48 a1i 
 |-  ( a e. ZZ -> ZZring e. Grp )
50 id 
 |-  ( a e. ZZ -> a e. ZZ )
51 3 a1i 
 |-  ( a e. ZZ -> 0 e. ZZ )
52 eqid 
 |-  ( invg ` ZZring ) = ( invg ` ZZring )
53 eqid 
 |-  ( invg ` R ) = ( invg ` R )
54 1 23 23 49 49 50 51 52 52 53 xpsinv 
 |-  ( a e. ZZ -> ( ( invg ` R ) ` <. a , 0 >. ) = <. ( ( invg ` ZZring ) ` a ) , ( ( invg ` ZZring ) ` 0 ) >. )
55 zringinvg 
 |-  ( a e. ZZ -> -u a = ( ( invg ` ZZring ) ` a ) )
56 znegcl 
 |-  ( a e. ZZ -> -u a e. ZZ )
57 55 56 eqeltrrd 
 |-  ( a e. ZZ -> ( ( invg ` ZZring ) ` a ) e. ZZ )
58 neg0 
 |-  -u 0 = 0
59 58 36 eqeltri 
 |-  -u 0 e. { 0 }
60 zringinvg 
 |-  ( 0 e. ZZ -> -u 0 = ( ( invg ` ZZring ) ` 0 ) )
61 60 eleq1d 
 |-  ( 0 e. ZZ -> ( -u 0 e. { 0 } <-> ( ( invg ` ZZring ) ` 0 ) e. { 0 } ) )
62 3 61 mp1i 
 |-  ( a e. ZZ -> ( -u 0 e. { 0 } <-> ( ( invg ` ZZring ) ` 0 ) e. { 0 } ) )
63 59 62 mpbii 
 |-  ( a e. ZZ -> ( ( invg ` ZZring ) ` 0 ) e. { 0 } )
64 57 63 opelxpd 
 |-  ( a e. ZZ -> <. ( ( invg ` ZZring ) ` a ) , ( ( invg ` ZZring ) ` 0 ) >. e. ( ZZ X. { 0 } ) )
65 54 64 eqeltrd 
 |-  ( a e. ZZ -> ( ( invg ` R ) ` <. a , 0 >. ) e. ( ZZ X. { 0 } ) )
66 65 adantr 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> ( ( invg ` R ) ` <. a , 0 >. ) e. ( ZZ X. { 0 } ) )
67 fveq2 
 |-  ( x = <. a , 0 >. -> ( ( invg ` R ) ` x ) = ( ( invg ` R ) ` <. a , 0 >. ) )
68 67 adantl 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> ( ( invg ` R ) ` x ) = ( ( invg ` R ) ` <. a , 0 >. ) )
69 2 a1i 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> I = ( ZZ X. { 0 } ) )
70 66 68 69 3eltr4d 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> ( ( invg ` R ) ` x ) e. I )
71 47 70 jca 
 |-  ( ( a e. ZZ /\ x = <. a , 0 >. ) -> ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) )
72 71 rexlimiva 
 |-  ( E. a e. ZZ x = <. a , 0 >. -> ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) )
73 17 72 sylbi 
 |-  ( x e. I -> ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) )
74 73 rgen 
 |-  A. x e. I ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I )
75 1 pzriprnglem1 
 |-  R e. Rng
76 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
77 75 76 ax-mp 
 |-  R e. Grp
78 eqid 
 |-  ( Base ` R ) = ( Base ` R )
79 78 34 53 issubg2 
 |-  ( R e. Grp -> ( I e. ( SubGrp ` R ) <-> ( I C_ ( Base ` R ) /\ I =/= (/) /\ A. x e. I ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) ) ) )
80 77 79 ax-mp 
 |-  ( I e. ( SubGrp ` R ) <-> ( I C_ ( Base ` R ) /\ I =/= (/) /\ A. x e. I ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) ) )
81 10 16 74 80 mpbir3an 
 |-  I e. ( SubGrp ` R )