Metamath Proof Explorer

Theorem isirred

Description: An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irred.1 
|- B = ( Base ` R )
irred.2 
|- U = ( Unit ` R )
irred.3 
|- I = ( Irred ` R )
irred.4 
|- N = ( B \ U )
irred.5 
|- .x. = ( .r ` R )
Assertion isirred 
|- ( X e. I <-> ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) )

Proof

Step Hyp Ref Expression
1 irred.1 
 |-  B = ( Base ` R )
2 irred.2 
 |-  U = ( Unit ` R )
3 irred.3 
 |-  I = ( Irred ` R )
4 irred.4 
 |-  N = ( B \ U )
5 irred.5 
 |-  .x. = ( .r ` R )
6 elfvdm 
 |-  ( X e. ( Irred ` R ) -> R e. dom Irred )
7 6 3 eleq2s 
 |-  ( X e. I -> R e. dom Irred )
8 7 elexd 
 |-  ( X e. I -> R e. _V )
9 eldifi 
 |-  ( X e. ( B \ U ) -> X e. B )
10 9 4 eleq2s 
 |-  ( X e. N -> X e. B )
11 10 1 eleqtrdi 
 |-  ( X e. N -> X e. ( Base ` R ) )
12 11 elfvexd 
 |-  ( X e. N -> R e. _V )
13 12 adantr 
 |-  ( ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) -> R e. _V )
14 fvex 
 |-  ( Base ` r ) e. _V
15 difexg 
 |-  ( ( Base ` r ) e. _V -> ( ( Base ` r ) \ ( Unit ` r ) ) e. _V )
16 14 15 mp1i 
 |-  ( r = R -> ( ( Base ` r ) \ ( Unit ` r ) ) e. _V )
17 simpr 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> b = ( ( Base ` r ) \ ( Unit ` r ) ) )
18 simpl 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> r = R )
19 18 fveq2d 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( Base ` r ) = ( Base ` R ) )
20 19 1 eqtr4di 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( Base ` r ) = B )
21 18 fveq2d 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( Unit ` r ) = ( Unit ` R ) )
22 21 2 eqtr4di 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( Unit ` r ) = U )
23 20 22 difeq12d 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( ( Base ` r ) \ ( Unit ` r ) ) = ( B \ U ) )
24 23 4 eqtr4di 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( ( Base ` r ) \ ( Unit ` r ) ) = N )
25 17 24 eqtrd 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> b = N )
26 18 fveq2d 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( .r ` r ) = ( .r ` R ) )
27 26 5 eqtr4di 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( .r ` r ) = .x. )
28 27 oveqd 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( x ( .r ` r ) y ) = ( x .x. y ) )
29 28 neeq1d 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( ( x ( .r ` r ) y ) =/= z <-> ( x .x. y ) =/= z ) )
30 25 29 raleqbidv 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( A. y e. b ( x ( .r ` r ) y ) =/= z <-> A. y e. N ( x .x. y ) =/= z ) )
31 25 30 raleqbidv 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> ( A. x e. b A. y e. b ( x ( .r ` r ) y ) =/= z <-> A. x e. N A. y e. N ( x .x. y ) =/= z ) )
32 25 31 rabeqbidv 
 |-  ( ( r = R /\ b = ( ( Base ` r ) \ ( Unit ` r ) ) ) -> { z e. b | A. x e. b A. y e. b ( x ( .r ` r ) y ) =/= z } = { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } )
33 16 32 csbied 
 |-  ( r = R -> [_ ( ( Base ` r ) \ ( Unit ` r ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` r ) y ) =/= z } = { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } )
34 df-irred 
 |-  Irred = ( r e. _V |-> [_ ( ( Base ` r ) \ ( Unit ` r ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` r ) y ) =/= z } )
35 fvex 
 |-  ( Base ` R ) e. _V
36 1 35 eqeltri 
 |-  B e. _V
37 36 difexi 
 |-  ( B \ U ) e. _V
38 4 37 eqeltri 
 |-  N e. _V
39 38 rabex 
 |-  { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } e. _V
40 33 34 39 fvmpt 
 |-  ( R e. _V -> ( Irred ` R ) = { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } )
41 3 40 syl5eq 
 |-  ( R e. _V -> I = { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } )
42 41 eleq2d 
 |-  ( R e. _V -> ( X e. I <-> X e. { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } ) )
43 neeq2 
 |-  ( z = X -> ( ( x .x. y ) =/= z <-> ( x .x. y ) =/= X ) )
44 43 2ralbidv 
 |-  ( z = X -> ( A. x e. N A. y e. N ( x .x. y ) =/= z <-> A. x e. N A. y e. N ( x .x. y ) =/= X ) )
45 44 elrab 
 |-  ( X e. { z e. N | A. x e. N A. y e. N ( x .x. y ) =/= z } <-> ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) )
46 42 45 bitrdi 
 |-  ( R e. _V -> ( X e. I <-> ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) ) )
47 8 13 46 pm5.21nii 
 |-  ( X e. I <-> ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) )