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