let R be Ring; :: thesis: ( R is almost_trivial iff ( R is degenerated or R, Z/ 2 are_isomorphic ) )
A1: Z/ 2 = doubleLoopStr(# (Segm 2),(),(),(In (1,(Segm 2))),(In (0,(Segm 2))) #) by INT_3:def 12;
A2: now :: thesis: ( ( R is degenerated or R, Z/ 2 are_isomorphic ) implies R is almost_trivial )
assume ( R is degenerated or R, Z/ 2 are_isomorphic ) ; :: thesis:
per cases ;
suppose R, Z/ 2 are_isomorphic ; :: thesis:
then consider f being Function of R,(Z/ 2) such that
A4: f is isomorphism by QUOFIELD:def 23;
( f is monomorphism & f is onto ) by ;
then A5: ( f is linear & f is one-to-one ) by MOD_4:def 8;
now :: thesis: for a being Element of R holds
( a = 1. R or a = 0. R )
let a be Element of R; :: thesis: ( b1 = 1. R or b1 = 0. R )
A6: dom f = [#] R by FUNCT_2:def 1;
A7: [#] () = 2 by ;
per cases ( f . a = 0 or f . a = 1 ) by ;
suppose f . a = 0 ; :: thesis: ( b1 = 1. R or b1 = 0. R )
then f . a = 0. (Z/ 2) by A1
.= f . (0. R) by ;
hence ( a = 1. R or a = 0. R ) by A5, A6; :: thesis: verum
end;
suppose f . a = 1 ; :: thesis: ( b1 = 1. R or b1 = 0. R )
then f . a = 1_ (Z/ 2) by INT_3:14
.= f . (1_ R) by
.= f . (1. R) ;
hence ( a = 1. R or a = 0. R ) by A5, A6; :: thesis: verum
end;
end;
end;
hence R is almost_trivial ; :: thesis: verum
end;
end;
end;
set A = the carrier of R;
set B = the carrier of (Z/ 2);
now :: thesis: ( R is almost_trivial & not R is degenerated implies R, Z/ 2 are_isomorphic )
assume that
A8: R is almost_trivial and
A9: not R is degenerated ; :: thesis:
set f = {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]};
now :: thesis: for o being object st o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} holds
o in [: the carrier of R, the carrier of (Z/ 2):]
let o be object ; :: thesis: ( o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} implies b1 in [: the carrier of R, the carrier of (Z/ 2):] )
assume o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} ; :: thesis: b1 in [: the carrier of R, the carrier of (Z/ 2):]
per cases then ( o = [(0. R),(0. (Z/ 2))] or o = [(1. R),(1. (Z/ 2))] ) by TARSKI:def 2;
suppose o = [(0. R),(0. (Z/ 2))] ; :: thesis: b1 in [: the carrier of R, the carrier of (Z/ 2):]
hence o in [: the carrier of R, the carrier of (Z/ 2):] by ZFMISC_1:def 2; :: thesis: verum
end;
suppose o = [(1. R),(1. (Z/ 2))] ; :: thesis: b1 in [: the carrier of R, the carrier of (Z/ 2):]
hence o in [: the carrier of R, the carrier of (Z/ 2):] by ZFMISC_1:def 2; :: thesis: verum
end;
end;
end;
then reconsider f = {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} as Subset of [: the carrier of R, the carrier of (Z/ 2):] by TARSKI:def 3;
reconsider f = f as Relation of the carrier of R, the carrier of (Z/ 2) ;
now :: thesis: for x, y1, y2 being object st [x,y1] in f & [x,y2] in f holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in f & [x,y2] in f implies b2 = b3 )
assume A11: ( [x,y1] in f & [x,y2] in f ) ; :: thesis: b2 = b3
per cases then ( [x,y1] = [(0. R),(0. (Z/ 2))] or [x,y1] = [(1. R),(1. (Z/ 2))] ) by TARSKI:def 2;
suppose A12: [x,y1] = [(0. R),(0. (Z/ 2))] ; :: thesis: b2 = b3
A13: y1 = [(0. R),(0. (Z/ 2))] `2 by A12
.= 0. (Z/ 2) ;
A14: x = [(0. R),(0. (Z/ 2))] `1 by A12
.= 0. R ;
per cases ( [x,y2] = [(0. R),(0. (Z/ 2))] or [x,y2] = [(1. R),(1. (Z/ 2))] ) by ;
suppose [x,y2] = [(0. R),(0. (Z/ 2))] ; :: thesis: b2 = b3
then y2 = [(0. R),(0. (Z/ 2))] `2
.= 0. (Z/ 2) ;
hence y1 = y2 by A13; :: thesis: verum
end;
suppose [x,y2] = [(1. R),(1. (Z/ 2))] ; :: thesis: b2 = b3
then x = [(1. R),(1. (Z/ 2))] `1
.= 1. R ;
hence y1 = y2 by ; :: thesis: verum
end;
end;
end;
suppose A15: [x,y1] = [(1. R),(1. (Z/ 2))] ; :: thesis: b2 = b3
then A16: y1 = [(1. R),(1. (Z/ 2))] `2
.= 1. (Z/ 2) ;
A17: x = [(1. R),(1. (Z/ 2))] `1 by A15
.= 1. R ;
per cases ( [x,y2] = [(0. R),(0. (Z/ 2))] or [x,y2] = [(1. R),(1. (Z/ 2))] ) by ;
suppose [x,y2] = [(0. R),(0. (Z/ 2))] ; :: thesis: b2 = b3
then x = [(0. R),(0. (Z/ 2))] `1
.= 0. R ;
hence y1 = y2 by ; :: thesis: verum
end;
suppose [x,y2] = [(1. R),(1. (Z/ 2))] ; :: thesis: b2 = b3
then y2 = [(1. R),(1. (Z/ 2))] `2
.= 1. (Z/ 2) ;
hence y1 = y2 by A16; :: thesis: verum
end;
end;
end;
end;
end;
then reconsider f = f as PartFunc of the carrier of R, the carrier of (Z/ 2) by FUNCT_1:def 1;
A18: dom f c= the carrier of R ;
now :: thesis: for o being object st o in the carrier of R holds
o in dom f
let o be object ; :: thesis: ( o in the carrier of R implies b1 in dom f )
assume o in the carrier of R ; :: thesis: b1 in dom f
then reconsider a = o as Element of R ;
end;
then A19: dom f = the carrier of R by ;
reconsider f = f as Function of the carrier of R, the carrier of (Z/ 2) by ;
A20: ( f . (0. R) = 0. (Z/ 2) & f . (1. R) = 1. (Z/ 2) )
proof
[(0. R),(0. (Z/ 2))] in f by TARSKI:def 2;
hence f . (0. R) = 0. (Z/ 2) by ; :: thesis: f . (1. R) = 1. (Z/ 2)
[(1. R),(1. (Z/ 2))] in f by TARSKI:def 2;
hence f . (1. R) = 1. (Z/ 2) by ; :: thesis: verum
end;
A21: now :: thesis: for a, b being Element of R holds f . (a + b) = (f . a) + (f . b)
let a, b be Element of R; :: thesis: f . (b1 + b2) = (f . b1) + (f . b2)
per cases ( a = 0. R or a = 1. R ) by A8;
suppose a = 0. R ; :: thesis: f . (b1 + b2) = (f . b1) + (f . b2)
hence f . (a + b) = (f . a) + (f . b) by A20; :: thesis: verum
end;
suppose A22: a = 1. R ; :: thesis: f . (b1 + b2) = (f . b1) + (f . b2)
per cases ( b = 0. R or b = 1. R ) by A8;
suppose b = 0. R ; :: thesis: f . (b1 + b2) = (f . b1) + (f . b2)
hence f . (a + b) = (f . a) + (f . b) by A20; :: thesis: verum
end;
suppose A23: b = 1. R ; :: thesis: f . (b1 + b2) = (f . b1) + (f . b2)
now :: thesis: not a + b = 1. R
assume A24: a + b = 1. R ; :: thesis: contradiction
consider y being Element of R such that
A25: a + y = 0. R by ALGSTR_0:def 11;
end;
hence f . (a + b) = (f . a) + (f . b) by A8, A20, Th5, A23, A22; :: thesis: verum
end;
end;
end;
end;
end;
now :: thesis: for a, b being Element of R holds f . (a * b) = (f . a) * (f . b)
let a, b be Element of R; :: thesis: f . (b1 * b2) = (f . b1) * (f . b2)
per cases ( a = 0. R or a = 1. R ) by A8;
suppose a = 0. R ; :: thesis: f . (b1 * b2) = (f . b1) * (f . b2)
hence f . (a * b) = (f . a) * (f . b) by A20; :: thesis: verum
end;
suppose a = 1. R ; :: thesis: f . (b1 * b2) = (f . b1) * (f . b2)
hence f . (a * b) = (f . a) * (f . b) by A20; :: thesis: verum
end;
end;
end;
then A28: ( f is additive & f is multiplicative & f is unity-preserving ) by ;
now :: thesis: for x, y being object st x in the carrier of R & y in the carrier of R & f . x = f . y holds
x = y
let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & f . x = f . y implies b1 = b2 )
assume A29: ( x in the carrier of R & y in the carrier of R & f . x = f . y ) ; :: thesis: b1 = b2
then reconsider a = x, b = y as Element of R ;
per cases ( a = 0. R or a = 1. R ) by A8;
suppose a = 0. R ; :: thesis: b1 = b2
hence x = y by A8, A20, A29; :: thesis: verum
end;
suppose a = 1. R ; :: thesis: b1 = b2
hence x = y by A8, A20, A29; :: thesis: verum
end;
end;
end;
then f is one-to-one by FUNCT_2:19;
then A30: f is monomorphism by ;
A31: now :: thesis: for o being object st o in rng f holds
o in the carrier of (Z/ 2)
let o be object ; :: thesis: ( o in rng f implies b1 in the carrier of (Z/ 2) )
assume o in rng f ; :: thesis: b1 in the carrier of (Z/ 2)
then consider x being object such that
A32: ( x in dom f & o = f . x ) by FUNCT_1:def 3;
reconsider a = x as Element of R by A32;
per cases ( a = 0. R or a = 1. R ) by A8;
suppose a = 0. R ; :: thesis: b1 in the carrier of (Z/ 2)
hence o in the carrier of (Z/ 2) by ; :: thesis: verum
end;
suppose a = 1. R ; :: thesis: b1 in the carrier of (Z/ 2)
hence o in the carrier of (Z/ 2) by ; :: thesis: verum
end;
end;
end;
now :: thesis: for o being object st o in the carrier of (Z/ 2) holds
o in rng f
let o be object ; :: thesis: ( o in the carrier of (Z/ 2) implies b1 in rng f )
assume o in the carrier of (Z/ 2) ; :: thesis: b1 in rng f
then A33: o in 2 by ;
per cases ( o = 0 or o = 1 ) by ;
suppose o = 0 ; :: thesis: b1 in rng f
then o = f . (0. R) by ;
hence o in rng f by ; :: thesis: verum
end;
suppose o = 1 ; :: thesis: b1 in rng f
then o = f . (1. R) by ;
hence o in rng f by ; :: thesis: verum
end;
end;
end;
then f is onto by ;
hence R, Z/ 2 are_isomorphic by ; :: thesis: verum
end;
hence ( R is almost_trivial iff ( R is degenerated or R, Z/ 2 are_isomorphic ) ) by A2; :: thesis: verum