Metamath Proof Explorer

Theorem pzriprnglem11

Description: Lemma 11 for pzriprng : The base set of the quotient of R and J . (Contributed by AV, 22-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 pzriprnglem11 
|- ( Base ` Q ) = U_ r e. ZZ { ( ZZ X. { r } ) }

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 df-qs 
 |-  ( ( ZZ X. ZZ ) /. .~ ) = { e | E. p e. ( ZZ X. ZZ ) e = [ p ] .~ }
8 6 a1i 
 |-  ( .~ = ( R ~QG I ) -> Q = ( R /s .~ ) )
9 1 pzriprnglem2 
 |-  ( Base ` R ) = ( ZZ X. ZZ )
10 9 eqcomi 
 |-  ( ZZ X. ZZ ) = ( Base ` R )
11 10 a1i 
 |-  ( .~ = ( R ~QG I ) -> ( ZZ X. ZZ ) = ( Base ` R ) )
12 ovexd 
 |-  ( .~ = ( R ~QG I ) -> ( R ~QG I ) e. _V )
13 5 12 eqeltrid 
 |-  ( .~ = ( R ~QG I ) -> .~ e. _V )
14 1 pzriprnglem1 
 |-  R e. Rng
15 14 a1i 
 |-  ( .~ = ( R ~QG I ) -> R e. Rng )
16 8 11 13 15 qusbas 
 |-  ( .~ = ( R ~QG I ) -> ( ( ZZ X. ZZ ) /. .~ ) = ( Base ` Q ) )
17 5 16 ax-mp 
 |-  ( ( ZZ X. ZZ ) /. .~ ) = ( Base ` Q )
18 nfcv 
 |-  F/_ s { e | e = [ p ] .~ }
19 nfcv 
 |-  F/_ r { e | e = [ p ] .~ }
20 nfcv 
 |-  F/_ p { e | e = [ <. s , r >. ] .~ }
21 eceq1 
 |-  ( p = <. s , r >. -> [ p ] .~ = [ <. s , r >. ] .~ )
22 21 eqeq2d 
 |-  ( p = <. s , r >. -> ( e = [ p ] .~ <-> e = [ <. s , r >. ] .~ ) )
23 22 abbidv 
 |-  ( p = <. s , r >. -> { e | e = [ p ] .~ } = { e | e = [ <. s , r >. ] .~ } )
24 18 19 20 23 iunxpf 
 |-  U_ p e. ( ZZ X. ZZ ) { e | e = [ p ] .~ } = U_ s e. ZZ U_ r e. ZZ { e | e = [ <. s , r >. ] .~ }
25 iunab 
 |-  U_ p e. ( ZZ X. ZZ ) { e | e = [ p ] .~ } = { e | E. p e. ( ZZ X. ZZ ) e = [ p ] .~ }
26 iuncom 
 |-  U_ s e. ZZ U_ r e. ZZ { e | e = [ <. s , r >. ] .~ } = U_ r e. ZZ U_ s e. ZZ { e | e = [ <. s , r >. ] .~ }
27 df-sn 
 |-  { [ <. s , r >. ] .~ } = { e | e = [ <. s , r >. ] .~ }
28 27 eqcomi 
 |-  { e | e = [ <. s , r >. ] .~ } = { [ <. s , r >. ] .~ }
29 28 a1i 
 |-  ( s e. ZZ -> { e | e = [ <. s , r >. ] .~ } = { [ <. s , r >. ] .~ } )
30 29 iuneq2i 
 |-  U_ s e. ZZ { e | e = [ <. s , r >. ] .~ } = U_ s e. ZZ { [ <. s , r >. ] .~ }
31 simpr 
 |-  ( ( ( r e. ZZ /\ s e. ZZ ) /\ p = [ <. s , r >. ] .~ ) -> p = [ <. s , r >. ] .~ )
32 1 2 3 4 5 pzriprnglem10 
 |-  ( ( s e. ZZ /\ r e. ZZ ) -> [ <. s , r >. ] .~ = ( ZZ X. { r } ) )
33 32 ancoms 
 |-  ( ( r e. ZZ /\ s e. ZZ ) -> [ <. s , r >. ] .~ = ( ZZ X. { r } ) )
34 33 adantr 
 |-  ( ( ( r e. ZZ /\ s e. ZZ ) /\ p = [ <. s , r >. ] .~ ) -> [ <. s , r >. ] .~ = ( ZZ X. { r } ) )
35 31 34 eqtrd 
 |-  ( ( ( r e. ZZ /\ s e. ZZ ) /\ p = [ <. s , r >. ] .~ ) -> p = ( ZZ X. { r } ) )
36 35 ex 
 |-  ( ( r e. ZZ /\ s e. ZZ ) -> ( p = [ <. s , r >. ] .~ -> p = ( ZZ X. { r } ) ) )
37 36 rexlimdva 
 |-  ( r e. ZZ -> ( E. s e. ZZ p = [ <. s , r >. ] .~ -> p = ( ZZ X. { r } ) ) )
38 0zd 
 |-  ( ( r e. ZZ /\ p = ( ZZ X. { r } ) ) -> 0 e. ZZ )
39 simpr 
 |-  ( ( r e. ZZ /\ p = ( ZZ X. { r } ) ) -> p = ( ZZ X. { r } ) )
40 opeq1 
 |-  ( s = 0 -> <. s , r >. = <. 0 , r >. )
41 40 eceq1d 
 |-  ( s = 0 -> [ <. s , r >. ] .~ = [ <. 0 , r >. ] .~ )
42 39 41 eqeqan12d 
 |-  ( ( ( r e. ZZ /\ p = ( ZZ X. { r } ) ) /\ s = 0 ) -> ( p = [ <. s , r >. ] .~ <-> ( ZZ X. { r } ) = [ <. 0 , r >. ] .~ ) )
43 0zd 
 |-  ( r e. ZZ -> 0 e. ZZ )
44 1 2 3 4 5 pzriprnglem10 
 |-  ( ( 0 e. ZZ /\ r e. ZZ ) -> [ <. 0 , r >. ] .~ = ( ZZ X. { r } ) )
45 43 44 mpancom 
 |-  ( r e. ZZ -> [ <. 0 , r >. ] .~ = ( ZZ X. { r } ) )
46 45 eqcomd 
 |-  ( r e. ZZ -> ( ZZ X. { r } ) = [ <. 0 , r >. ] .~ )
47 46 adantr 
 |-  ( ( r e. ZZ /\ p = ( ZZ X. { r } ) ) -> ( ZZ X. { r } ) = [ <. 0 , r >. ] .~ )
48 38 42 47 rspcedvd 
 |-  ( ( r e. ZZ /\ p = ( ZZ X. { r } ) ) -> E. s e. ZZ p = [ <. s , r >. ] .~ )
49 48 ex 
 |-  ( r e. ZZ -> ( p = ( ZZ X. { r } ) -> E. s e. ZZ p = [ <. s , r >. ] .~ ) )
50 37 49 impbid 
 |-  ( r e. ZZ -> ( E. s e. ZZ p = [ <. s , r >. ] .~ <-> p = ( ZZ X. { r } ) ) )
51 50 abbidv 
 |-  ( r e. ZZ -> { p | E. s e. ZZ p = [ <. s , r >. ] .~ } = { p | p = ( ZZ X. { r } ) } )
52 iunsn 
 |-  U_ s e. ZZ { [ <. s , r >. ] .~ } = { p | E. s e. ZZ p = [ <. s , r >. ] .~ }
53 df-sn 
 |-  { ( ZZ X. { r } ) } = { p | p = ( ZZ X. { r } ) }
54 51 52 53 3eqtr4g 
 |-  ( r e. ZZ -> U_ s e. ZZ { [ <. s , r >. ] .~ } = { ( ZZ X. { r } ) } )
55 30 54 eqtrid 
 |-  ( r e. ZZ -> U_ s e. ZZ { e | e = [ <. s , r >. ] .~ } = { ( ZZ X. { r } ) } )
56 55 iuneq2i 
 |-  U_ r e. ZZ U_ s e. ZZ { e | e = [ <. s , r >. ] .~ } = U_ r e. ZZ { ( ZZ X. { r } ) }
57 26 56 eqtri 
 |-  U_ s e. ZZ U_ r e. ZZ { e | e = [ <. s , r >. ] .~ } = U_ r e. ZZ { ( ZZ X. { r } ) }
58 24 25 57 3eqtr3i 
 |-  { e | E. p e. ( ZZ X. ZZ ) e = [ p ] .~ } = U_ r e. ZZ { ( ZZ X. { r } ) }
59 7 17 58 3eqtr3i 
 |-  ( Base ` Q ) = U_ r e. ZZ { ( ZZ X. { r } ) }