let R be Skew-Field; :: thesis: the carrier of () = the carrier of (center ()) \/ {(0. R)}
A1: the carrier of (center ()) c= the carrier of () by GROUP_2:def 5;
A2: the carrier of () = NonZero R by UNIROOTS:def 1;
A3: the carrier of () \/ {(0. R)} = the carrier of R by UNIROOTS:15;
A4: the carrier of () c= the carrier of R by Th16;
A5: the carrier of (center ()) \/ {(0. R)} c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (center ()) \/ {(0. R)} or x in the carrier of () )
assume A6: x in the carrier of (center ()) \/ {(0. R)} ; :: thesis: x in the carrier of ()
per cases ( x in the carrier of (center ()) or x in {(0. R)} ) by ;
suppose A7: x in the carrier of (center ()) ; :: thesis: x in the carrier of ()
then reconsider a = x as Element of () by A1;
A8: a in center () by A7;
reconsider a1 = a as Element of R by UNIROOTS:19;
now :: thesis: for b being Element of R holds a1 * b = b * a1
let b be Element of R; :: thesis: a1 * b = b * a1
thus a1 * b = b * a1 :: thesis: verum
proof
per cases ( b in the carrier of () or b in {(0. R)} ) by ;
suppose b in the carrier of () ; :: thesis: a1 * b = b * a1
then reconsider b1 = b as Element of () ;
thus a1 * b = a * b1 by UNIROOTS:16
.= b1 * a by
.= b * a1 by UNIROOTS:16 ; :: thesis: verum
end;
suppose b in {(0. R)} ; :: thesis: a1 * b = b * a1
then A9: b = 0. R by TARSKI:def 1;
hence a1 * b = 0. R
.= b * a1 by A9 ;
:: thesis: verum
end;
end;
end;
end;
then a1 in center R by Th17;
hence x in the carrier of () ; :: thesis: verum
end;
end;
end;
the carrier of () c= the carrier of (center ()) \/ {(0. R)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in the carrier of (center ()) \/ {(0. R)} )
assume A10: x in the carrier of () ; :: thesis: x in the carrier of (center ()) \/ {(0. R)}
then reconsider a = x as Element of () ;
reconsider a1 = a as Element of R by A4;
per cases ( a1 = 0. R or a1 <> 0. R ) ;
suppose a1 <> 0. R ; :: thesis: x in the carrier of (center ()) \/ {(0. R)}
then not a1 in {(0. R)} by TARSKI:def 1;
then reconsider a2 = a1 as Element of () by ;
now :: thesis: for b being Element of () holds a2 * b = b * a2
let b be Element of (); :: thesis: a2 * b = b * a2
b in the carrier of () ;
then reconsider b1 = b as Element of R by A2;
A11: x in center R by A10;
thus a2 * b = a1 * b1 by UNIROOTS:16
.= b1 * a1 by
.= b * a2 by UNIROOTS:16 ; :: thesis: verum
end;
then a1 in center () by GROUP_5:77;
then a1 in the carrier of (center ()) ;
hence x in the carrier of (center ()) \/ {(0. R)} by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence the carrier of () = the carrier of (center ()) \/ {(0. R)} by ; :: thesis: verum