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),(addint 2),(multint 2),(In (1,(Segm 2))),(In (0,(Segm 2))) #) by INT_3:def 12;

set B = the carrier of (Z/ 2);

A1: Z/ 2 = doubleLoopStr(# (Segm 2),(addint 2),(multint 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 )

set A = the carrier of R;assume
( R is degenerated or R, Z/ 2 are_isomorphic )
; :: thesis: R is almost_trivial

end;per cases then
( R is degenerated or R, Z/ 2 are_isomorphic )
;

end;

suppose
R, Z/ 2 are_isomorphic
; :: thesis: R is almost_trivial

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 A4, MOD_4:def 12;

then A5: ( f is linear & f is one-to-one ) by MOD_4:def 8;

end;A4: f is isomorphism by QUOFIELD:def 23;

( f is monomorphism & f is onto ) by A4, MOD_4:def 12;

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 )

hence
R is almost_trivial
; :: thesis: verum( a = 1. R or a = 0. R )

let a be Element of R; :: thesis: ( b_{1} = 1. R or b_{1} = 0. R )

A6: dom f = [#] R by FUNCT_2:def 1;

A7: [#] (INT.Ring 2) = 2 by A1, ORDINAL1:def 17;

end;A6: dom f = [#] R by FUNCT_2:def 1;

A7: [#] (INT.Ring 2) = 2 by A1, ORDINAL1:def 17;

set B = the carrier of (Z/ 2);

now :: thesis: ( R is almost_trivial & not R is degenerated implies R, Z/ 2 are_isomorphic )

hence
( R is almost_trivial iff ( R is degenerated or R, Z/ 2 are_isomorphic ) )
by A2; :: thesis: verumassume that

A8: R is almost_trivial and

A9: not R is degenerated ; :: thesis: R, Z/ 2 are_isomorphic

set f = {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]};

reconsider f = f as Relation of the carrier of R, the carrier of (Z/ 2) ;

A18: dom f c= the carrier of R ;

reconsider f = f as Function of the carrier of R, the carrier of (Z/ 2) by A19, FUNCT_2:def 1;

A20: ( f . (0. R) = 0. (Z/ 2) & f . (1. R) = 1. (Z/ 2) )

then A30: f is monomorphism by A28, MOD_4:def 8;

hence R, Z/ 2 are_isomorphic by A30, MOD_4:def 12, QUOFIELD:def 23; :: thesis: verum

end;A8: R is almost_trivial and

A9: not R is degenerated ; :: thesis: R, Z/ 2 are_isomorphic

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

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;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 b_{1} in [: the carrier of R, the carrier of (Z/ 2):] )

assume o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} ; :: thesis: b_{1} in [: the carrier of R, the carrier of (Z/ 2):]

end;assume o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} ; :: thesis: b

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

then reconsider f = f as PartFunc of the carrier of R, the carrier of (Z/ 2) by FUNCT_1:def 1;y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in f & [x,y2] in f implies b_{2} = b_{3} )

assume A11: ( [x,y1] in f & [x,y2] in f ) ; :: thesis: b_{2} = b_{3}

end;assume A11: ( [x,y1] in f & [x,y2] in f ) ; :: thesis: b

per cases then
( [x,y1] = [(0. R),(0. (Z/ 2))] or [x,y1] = [(1. R),(1. (Z/ 2))] )
by TARSKI:def 2;

end;

suppose A12:
[x,y1] = [(0. R),(0. (Z/ 2))]
; :: thesis: b_{2} = b_{3}

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 ;

end;.= 0. (Z/ 2) ;

A14: x = [(0. R),(0. (Z/ 2))] `1 by A12

.= 0. R ;

suppose A15:
[x,y1] = [(1. R),(1. (Z/ 2))]
; :: thesis: b_{2} = b_{3}

then A16: y1 =
[(1. R),(1. (Z/ 2))] `2

.= 1. (Z/ 2) ;

A17: x = [(1. R),(1. (Z/ 2))] `1 by A15

.= 1. R ;

end;.= 1. (Z/ 2) ;

A17: x = [(1. R),(1. (Z/ 2))] `1 by A15

.= 1. R ;

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

then A19:
dom f = the carrier of R
by A18, TARSKI:2;o in dom f

let o be object ; :: thesis: ( o in the carrier of R implies b_{1} in dom f )

assume o in the carrier of R ; :: thesis: b_{1} in dom f

then reconsider a = o as Element of R ;

end;assume o in the carrier of R ; :: thesis: b

then reconsider a = o as Element of R ;

reconsider f = f as Function of the carrier of R, the carrier of (Z/ 2) by A19, FUNCT_2:def 1;

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 A19, FUNCT_1:def 2; :: 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 A19, FUNCT_1:def 2; :: thesis: verum

end;hence f . (0. R) = 0. (Z/ 2) by A19, FUNCT_1:def 2; :: 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 A19, FUNCT_1:def 2; :: thesis: verum

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 . (b_{1} + b_{2}) = (f . b_{1}) + (f . b_{2})

end;per cases
( a = 0. R or a = 1. R )
by A8;

end;

suppose A22:
a = 1. R
; :: thesis: f . (b_{1} + b_{2}) = (f . b_{1}) + (f . b_{2})

end;

per cases
( b = 0. R or b = 1. R )
by A8;

end;

suppose A23:
b = 1. R
; :: thesis: f . (b_{1} + b_{2}) = (f . b_{1}) + (f . b_{2})

end;

now :: thesis: not a + b = 1. R

hence
f . (a + b) = (f . a) + (f . b)
by A8, A20, Th5, A23, A22; :: thesis: verumassume 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;consider y being Element of R such that

A25: a + y = 0. R by ALGSTR_0:def 11;

now :: thesis: for a, b being Element of R holds f . (a * b) = (f . a) * (f . b)

then A28:
( f is additive & f is multiplicative & f is unity-preserving )
by A20, A21, GROUP_6:def 6;let a, b be Element of R; :: thesis: f . (b_{1} * b_{2}) = (f . b_{1}) * (f . b_{2})

end;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

then
f is one-to-one
by FUNCT_2:19;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 b_{1} = b_{2} )

assume A29: ( x in the carrier of R & y in the carrier of R & f . x = f . y ) ; :: thesis: b_{1} = b_{2}

then reconsider a = x, b = y as Element of R ;

end;assume A29: ( x in the carrier of R & y in the carrier of R & f . x = f . y ) ; :: thesis: b

then reconsider a = x, b = y as Element of R ;

then A30: f is monomorphism by A28, MOD_4:def 8;

A31: now :: thesis: for o being object st o in rng f holds

o in the carrier of (Z/ 2)

o in the carrier of (Z/ 2)

let o be object ; :: thesis: ( o in rng f implies b_{1} in the carrier of (Z/ 2) )

assume o in rng f ; :: thesis: b_{1} 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;

end;assume o in rng f ; :: thesis: b

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;

now :: thesis: for o being object st o in the carrier of (Z/ 2) holds

o in rng f

then
f is onto
by A31, TARSKI:2;o in rng f

let o be object ; :: thesis: ( o in the carrier of (Z/ 2) implies b_{1} in rng f )

assume o in the carrier of (Z/ 2) ; :: thesis: b_{1} in rng f

then A33: o in 2 by A1, ORDINAL1:def 17;

end;assume o in the carrier of (Z/ 2) ; :: thesis: b

then A33: o in 2 by A1, ORDINAL1:def 17;

per cases
( o = 0 or o = 1 )
by A33, CARD_1:50, TARSKI:def 2;

end;

suppose
o = 0
; :: thesis: b_{1} in rng f

then
o = f . (0. R)
by A1, A20, NAT_1:44, SUBSET_1:def 8;

hence o in rng f by A19, FUNCT_1:def 3; :: thesis: verum

end;hence o in rng f by A19, FUNCT_1:def 3; :: thesis: verum

suppose
o = 1
; :: thesis: b_{1} in rng f

then
o = f . (1. R)
by A20, A1, NAT_1:44, SUBSET_1:def 8;

hence o in rng f by A19, FUNCT_1:def 3; :: thesis: verum

end;hence o in rng f by A19, FUNCT_1:def 3; :: thesis: verum

hence R, Z/ 2 are_isomorphic by A30, MOD_4:def 12, QUOFIELD:def 23; :: thesis: verum