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 eqtrid
 |-  ( 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 ) )