:: QUOFIELD semantic presentation
begin
definition
let I be non empty ZeroStr ;
func Q. I -> Subset of [: the carrier of I, the carrier of I:] means :Def1: :: QUOFIELD:def 1
for u being set holds
( u in it iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) );
existence
ex b1 being Subset of [: the carrier of I, the carrier of I:] st
for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) )
proof
set M = { [a,b] where a, b is Element of I : b <> 0. I } ;
for u being set st u in { [a,b] where a, b is Element of I : b <> 0. I } holds
u in [: the carrier of I, the carrier of I:]
proof
let u be set ; ::_thesis: ( u in { [a,b] where a, b is Element of I : b <> 0. I } implies u in [: the carrier of I, the carrier of I:] )
assume u in { [a,b] where a, b is Element of I : b <> 0. I } ; ::_thesis: u in [: the carrier of I, the carrier of I:]
then ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ;
hence u in [: the carrier of I, the carrier of I:] ; ::_thesis: verum
end;
then A1: { [a,b] where a, b is Element of I : b <> 0. I } is Subset of [: the carrier of I, the carrier of I:] by TARSKI:def_3;
for u being set holds
( u in { [a,b] where a, b is Element of I : b <> 0. I } iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ;
hence ex b1 being Subset of [: the carrier of I, the carrier of I:] st
for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of [: the carrier of I, the carrier of I:] st ( for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds
( u in b2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) holds
b1 = b2
proof
let M1, M2 be Subset of [: the carrier of I, the carrier of I:]; ::_thesis: ( ( for u being set holds
( u in M1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds
( u in M2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) implies M1 = M2 )
assume A2: for u being set holds
( u in M1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ; ::_thesis: ( ex u being set st
( ( u in M2 implies ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) implies ( ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) & not u in M2 ) ) or M1 = M2 )
assume A3: for u being set holds
( u in M2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ; ::_thesis: M1 = M2
A4: for u being set st u in M2 holds
u in M1
proof
let u be set ; ::_thesis: ( u in M2 implies u in M1 )
assume u in M2 ; ::_thesis: u in M1
then ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) by A3;
hence u in M1 by A2; ::_thesis: verum
end;
for u being set st u in M1 holds
u in M2
proof
let u be set ; ::_thesis: ( u in M1 implies u in M2 )
assume u in M1 ; ::_thesis: u in M2
then ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) by A2;
hence u in M2 by A3; ::_thesis: verum
end;
hence M1 = M2 by A4, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Q. QUOFIELD:def_1_:_
for I being non empty ZeroStr
for b2 being Subset of [: the carrier of I, the carrier of I:] holds
( b2 = Q. I iff for u being set holds
( u in b2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) );
theorem Th1: :: QUOFIELD:1
for I being non empty non degenerated multLoopStr_0 holds not Q. I is empty
proof
let I be non empty non degenerated multLoopStr_0 ; ::_thesis: not Q. I is empty
1. I <> 0. I ;
then [(1. I),(1. I)] in Q. I by Def1;
hence not Q. I is empty ; ::_thesis: verum
end;
registration
let I be non empty non degenerated multLoopStr_0 ;
cluster Q. I -> non empty ;
coherence
not Q. I is empty by Th1;
end;
theorem Th2: :: QUOFIELD:2
for I being non empty non degenerated multLoopStr_0
for u being Element of Q. I holds u `2 <> 0. I
proof
let I be non empty non degenerated multLoopStr_0 ; ::_thesis: for u being Element of Q. I holds u `2 <> 0. I
let u be Element of Q. I; ::_thesis: u `2 <> 0. I
ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) by Def1;
hence u `2 <> 0. I by MCART_1:7; ::_thesis: verum
end;
definition
let I be non empty non degenerated domRing-like doubleLoopStr ;
let u, v be Element of Q. I;
func padd (u,v) -> Element of Q. I equals :: QUOFIELD:def 2
[(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))];
coherence
[(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Q. I
proof
( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then (u `2) * (v `2) <> 0. I by VECTSP_2:def_1;
hence [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Q. I by Def1; ::_thesis: verum
end;
end;
:: deftheorem defines padd QUOFIELD:def_2_:_
for I being non empty non degenerated domRing-like doubleLoopStr
for u, v being Element of Q. I holds padd (u,v) = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))];
definition
let I be non empty non degenerated domRing-like doubleLoopStr ;
let u, v be Element of Q. I;
func pmult (u,v) -> Element of Q. I equals :: QUOFIELD:def 3
[((u `1) * (v `1)),((u `2) * (v `2))];
coherence
[((u `1) * (v `1)),((u `2) * (v `2))] is Element of Q. I
proof
( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then (u `2) * (v `2) <> 0. I by VECTSP_2:def_1;
hence [((u `1) * (v `1)),((u `2) * (v `2))] is Element of Q. I by Def1; ::_thesis: verum
end;
end;
:: deftheorem defines pmult QUOFIELD:def_3_:_
for I being non empty non degenerated domRing-like doubleLoopStr
for u, v being Element of Q. I holds pmult (u,v) = [((u `1) * (v `1)),((u `2) * (v `2))];
theorem Th3: :: QUOFIELD:3
for I being non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr
for u, v, w being Element of Q. I holds padd (u,(padd (v,w))) = padd ((padd (u,v)),w)
proof
let I be non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr ; ::_thesis: for u, v, w being Element of Q. I holds padd (u,(padd (v,w))) = padd ((padd (u,v)),w)
let u, v, w be Element of Q. I; ::_thesis: padd (u,(padd (v,w))) = padd ((padd (u,v)),w)
A1: ((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2)) = ((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) * (u `2)) + (((w `1) * (v `2)) * (u `2))) by VECTSP_1:def_3
.= (((u `1) * ((v `2) * (w `2))) + (((v `1) * (w `2)) * (u `2))) + (((w `1) * (v `2)) * (u `2)) by RLVECT_1:def_3
.= (((u `1) * ((v `2) * (w `2))) + (((v `1) * (w `2)) * (u `2))) + ((w `1) * ((v `2) * (u `2))) by GROUP_1:def_3
.= ((((u `1) * (v `2)) * (w `2)) + (((v `1) * (w `2)) * (u `2))) + ((w `1) * ((v `2) * (u `2))) by GROUP_1:def_3
.= ((((u `1) * (v `2)) * (w `2)) + (((v `1) * (u `2)) * (w `2))) + ((w `1) * ((v `2) * (u `2))) by GROUP_1:def_3
.= ((((u `1) * (v `2)) + ((v `1) * (u `2))) * (w `2)) + ((w `1) * ((v `2) * (u `2))) by VECTSP_1:def_3 ;
A2: v `2 <> 0. I by Th2;
X1: ( [(((v `1) * (w `2)) + ((w `1) * (v `2))),((v `2) * (w `2))] `1 = ((v `1) * (w `2)) + ((w `1) * (v `2)) & [(((v `1) * (w `2)) + ((w `1) * (v `2))),((v `2) * (w `2))] `2 = (v `2) * (w `2) ) ;
X2: ( [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] `1 = ((u `1) * (v `2)) + ((v `1) * (u `2)) & [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
u `2 <> 0. I by Th2;
then (u `2) * (v `2) <> 0. I by A2, VECTSP_2:def_1;
then reconsider s = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] as Element of Q. I by Def1;
w `2 <> 0. I by Th2;
then (v `2) * (w `2) <> 0. I by A2, VECTSP_2:def_1;
then reconsider t = [(((v `1) * (w `2)) + ((w `1) * (v `2))),((v `2) * (w `2))] as Element of Q. I by Def1;
padd (u,(padd (v,w))) = [(((u `1) * (t `2)) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),((u `2) * (t `2))] by X1
.= [(((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),((u `2) * (t `2))] by X1
.= [(((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),((u `2) * ((v `2) * (w `2)))] by X1
.= [(((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),(((u `2) * (v `2)) * (w `2))] by GROUP_1:def_3 ;
then padd (u,(padd (v,w))) = [(((s `1) * (w `2)) + ((w `1) * ((v `2) * (u `2)))),(((u `2) * (v `2)) * (w `2))] by A1, X2
.= [(((s `1) * (w `2)) + ((w `1) * (s `2))),(((u `2) * (v `2)) * (w `2))] by X2
.= padd ((padd (u,v)),w) by X2 ;
hence padd (u,(padd (v,w))) = padd ((padd (u,v)),w) ; ::_thesis: verum
end;
theorem Th4: :: QUOFIELD:4
for I being non empty non degenerated Abelian associative commutative domRing-like doubleLoopStr
for u, v, w being Element of Q. I holds pmult (u,(pmult (v,w))) = pmult ((pmult (u,v)),w)
proof
let I be non empty non degenerated Abelian associative commutative domRing-like doubleLoopStr ; ::_thesis: for u, v, w being Element of Q. I holds pmult (u,(pmult (v,w))) = pmult ((pmult (u,v)),w)
let u, v, w be Element of Q. I; ::_thesis: pmult (u,(pmult (v,w))) = pmult ((pmult (u,v)),w)
A1: v `2 <> 0. I by Th2;
w `2 <> 0. I by Th2;
then (v `2) * (w `2) <> 0. I by A1, VECTSP_2:def_1;
then reconsider t = [((v `1) * (w `1)),((v `2) * (w `2))] as Element of Q. I by Def1;
u `2 <> 0. I by Th2;
then (u `2) * (v `2) <> 0. I by A1, VECTSP_2:def_1;
then reconsider s = [((u `1) * (v `1)),((u `2) * (v `2))] as Element of Q. I by Def1;
X2: ( [((u `1) * (v `1)),((u `2) * (v `2))] `1 = (u `1) * (v `1) & [((u `1) * (v `1)),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
X1: ( [((v `1) * (w `1)),((v `2) * (w `2))] `1 = (v `1) * (w `1) & [((v `1) * (w `1)),((v `2) * (w `2))] `2 = (v `2) * (w `2) ) ;
pmult (u,(pmult (v,w))) = [((u `1) * ((v `1) * (w `1))),((u `2) * (t `2))] by X1
.= [((u `1) * ((v `1) * (w `1))),((u `2) * ((v `2) * (w `2)))] by X1
.= [(((u `1) * (v `1)) * (w `1)),((u `2) * ((v `2) * (w `2)))] by GROUP_1:def_3
.= [(((u `1) * (v `1)) * (w `1)),(((u `2) * (v `2)) * (w `2))] by GROUP_1:def_3
.= [((s `1) * (w `1)),(((u `2) * (v `2)) * (w `2))] by X2
.= pmult ((pmult (u,v)),w) by X2 ;
hence pmult (u,(pmult (v,w))) = pmult ((pmult (u,v)),w) ; ::_thesis: verum
end;
definition
let I be non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr ;
let u, v be Element of Q. I;
:: original: padd
redefine func padd (u,v) -> Element of Q. I;
commutativity
for u, v being Element of Q. I holds padd (u,v) = padd (v,u)
proof
let u, v be Element of Q. I; ::_thesis: padd (u,v) = padd (v,u)
thus padd (u,v) = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))]
.= padd (v,u) ; ::_thesis: verum
end;
end;
definition
let I be non empty non degenerated Abelian associative commutative domRing-like doubleLoopStr ;
let u, v be Element of Q. I;
:: original: pmult
redefine func pmult (u,v) -> Element of Q. I;
commutativity
for u, v being Element of Q. I holds pmult (u,v) = pmult (v,u)
proof
let u, v be Element of Q. I; ::_thesis: pmult (u,v) = pmult (v,u)
thus pmult (u,v) = [((u `1) * (v `1)),((u `2) * (v `2))]
.= pmult (v,u) ; ::_thesis: verum
end;
end;
definition
let I be non empty non degenerated multLoopStr_0 ;
let u be Element of Q. I;
func QClass. u -> Subset of (Q. I) means :Def4: :: QUOFIELD:def 4
for z being Element of Q. I holds
( z in it iff (z `1) * (u `2) = (z `2) * (u `1) );
existence
ex b1 being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b1 iff (z `1) * (u `2) = (z `2) * (u `1) )
proof
set M = { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } ;
for x being Element of Q. I st x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } holds
(x `1) * (u `2) = (x `2) * (u `1)
proof
let x be Element of Q. I; ::_thesis: ( x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } implies (x `1) * (u `2) = (x `2) * (u `1) )
assume x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } ; ::_thesis: (x `1) * (u `2) = (x `2) * (u `1)
then ex z being Element of Q. I st
( x = z & (z `1) * (u `2) = (z `2) * (u `1) ) ;
hence (x `1) * (u `2) = (x `2) * (u `1) ; ::_thesis: verum
end;
then A1: for x being Element of Q. I holds
( x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } iff (x `1) * (u `2) = (x `2) * (u `1) ) ;
for x being set st x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } holds
x in Q. I
proof
let x be set ; ::_thesis: ( x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } implies x in Q. I )
assume x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } ; ::_thesis: x in Q. I
then ex z being Element of Q. I st
( x = z & (z `1) * (u `2) = (z `2) * (u `1) ) ;
hence x in Q. I ; ::_thesis: verum
end;
then { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } is Subset of (Q. I) by TARSKI:def_3;
hence ex b1 being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b1 iff (z `1) * (u `2) = (z `2) * (u `1) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (Q. I) st ( for z being Element of Q. I holds
( z in b1 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) & ( for z being Element of Q. I holds
( z in b2 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) holds
b1 = b2
proof
let M1, M2 be Subset of (Q. I); ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) & ( for z being Element of Q. I holds
( z in M2 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) implies M1 = M2 )
assume A2: for z being Element of Q. I holds
( z in M1 iff (z `1) * (u `2) = (z `2) * (u `1) ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies (z `1) * (u `2) = (z `2) * (u `1) ) implies ( (z `1) * (u `2) = (z `2) * (u `1) & not z in M2 ) ) or M1 = M2 )
assume A3: for z being Element of Q. I holds
( z in M2 iff (z `1) * (u `2) = (z `2) * (u `1) ) ; ::_thesis: M1 = M2
A4: for x being set st x in M2 holds
x in M1
proof
let x be set ; ::_thesis: ( x in M2 implies x in M1 )
assume A5: x in M2 ; ::_thesis: x in M1
then reconsider x = x as Element of Q. I ;
(x `1) * (u `2) = (x `2) * (u `1) by A3, A5;
hence x in M1 by A2; ::_thesis: verum
end;
for x being set st x in M1 holds
x in M2
proof
let x be set ; ::_thesis: ( x in M1 implies x in M2 )
assume A6: x in M1 ; ::_thesis: x in M2
then reconsider x = x as Element of Q. I ;
(x `1) * (u `2) = (x `2) * (u `1) by A2, A6;
hence x in M2 by A3; ::_thesis: verum
end;
hence M1 = M2 by A4, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines QClass. QUOFIELD:def_4_:_
for I being non empty non degenerated multLoopStr_0
for u being Element of Q. I
for b3 being Subset of (Q. I) holds
( b3 = QClass. u iff for z being Element of Q. I holds
( z in b3 iff (z `1) * (u `2) = (z `2) * (u `1) ) );
theorem Th5: :: QUOFIELD:5
for I being non empty non degenerated commutative multLoopStr_0
for u being Element of Q. I holds u in QClass. u
proof
let I be non empty non degenerated commutative multLoopStr_0 ; ::_thesis: for u being Element of Q. I holds u in QClass. u
let u be Element of Q. I; ::_thesis: u in QClass. u
(u `1) * (u `2) = (u `1) * (u `2) ;
hence u in QClass. u by Def4; ::_thesis: verum
end;
registration
let I be non empty non degenerated commutative multLoopStr_0 ;
let u be Element of Q. I;
cluster QClass. u -> non empty ;
coherence
not QClass. u is empty by Th5;
end;
definition
let I be non empty non degenerated multLoopStr_0 ;
func Quot. I -> Subset-Family of (Q. I) means :Def5: :: QUOFIELD:def 5
for A being Subset of (Q. I) holds
( A in it iff ex u being Element of Q. I st A = QClass. u );
existence
ex b1 being Subset-Family of (Q. I) st
for A being Subset of (Q. I) holds
( A in b1 iff ex u being Element of Q. I st A = QClass. u )
proof
defpred S1[ set ] means ex u being Element of Q. I st $1 = QClass. u;
thus ex S being Subset-Family of (Q. I) st
for A being Subset of (Q. I) holds
( A in S iff S1[A] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of (Q. I) st ( for A being Subset of (Q. I) holds
( A in b1 iff ex u being Element of Q. I st A = QClass. u ) ) & ( for A being Subset of (Q. I) holds
( A in b2 iff ex u being Element of Q. I st A = QClass. u ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex a being Element of Q. I st $1 = QClass. a;
let F1, F2 be Subset-Family of (Q. I); ::_thesis: ( ( for A being Subset of (Q. I) holds
( A in F1 iff ex u being Element of Q. I st A = QClass. u ) ) & ( for A being Subset of (Q. I) holds
( A in F2 iff ex u being Element of Q. I st A = QClass. u ) ) implies F1 = F2 )
assume A1: for A being Subset of (Q. I) holds
( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of (Q. I) st
( ( A in F2 implies ex u being Element of Q. I st A = QClass. u ) implies ( ex u being Element of Q. I st A = QClass. u & not A in F2 ) ) or F1 = F2 )
assume A2: for A being Subset of (Q. I) holds
( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2
thus F1 = F2 from SUBSET_1:sch_4(A1, A2); ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Quot. QUOFIELD:def_5_:_
for I being non empty non degenerated multLoopStr_0
for b2 being Subset-Family of (Q. I) holds
( b2 = Quot. I iff for A being Subset of (Q. I) holds
( A in b2 iff ex u being Element of Q. I st A = QClass. u ) );
theorem Th6: :: QUOFIELD:6
for I being non empty non degenerated multLoopStr_0 holds not Quot. I is empty
proof
let I be non empty non degenerated multLoopStr_0 ; ::_thesis: not Quot. I is empty
1. I <> 0. I ;
then reconsider u = [(1. I),(1. I)] as Element of Q. I by Def1;
QClass. u in Quot. I by Def5;
hence not Quot. I is empty ; ::_thesis: verum
end;
registration
let I be non empty non degenerated multLoopStr_0 ;
cluster Quot. I -> non empty ;
coherence
not Quot. I is empty by Th6;
end;
theorem Th7: :: QUOFIELD:7
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Q. I st ex w being Element of Quot. I st
( u in w & v in w ) holds
(u `1) * (v `2) = (v `1) * (u `2)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of Q. I st ex w being Element of Quot. I st
( u in w & v in w ) holds
(u `1) * (v `2) = (v `1) * (u `2)
let u, v be Element of Q. I; ::_thesis: ( ex w being Element of Quot. I st
( u in w & v in w ) implies (u `1) * (v `2) = (v `1) * (u `2) )
given w being Element of Quot. I such that A1: u in w and
A2: v in w ; ::_thesis: (u `1) * (v `2) = (v `1) * (u `2)
consider z being Element of Q. I such that
A3: w = QClass. z by Def5;
A4: (u `1) * (z `2) = (z `1) * (u `2) by A1, A3, Def4;
z `2 divides z `2 ;
then A5: z `2 divides ((v `2) * (u `1)) * (z `2) by GCD_1:7;
A6: (v `1) * (z `2) = (z `1) * (v `2) by A2, A3, Def4;
then A7: z `2 divides (z `1) * (v `2) by GCD_1:def_1;
then A8: z `2 divides ((z `1) * (v `2)) * (u `2) by GCD_1:7;
A9: z `2 <> 0. I by Th2;
hence (v `1) * (u `2) = (((z `1) * (v `2)) / (z `2)) * (u `2) by A6, A7, GCD_1:def_4
.= (((z `1) * (v `2)) * (u `2)) / (z `2) by A7, A8, A9, GCD_1:11
.= ((v `2) * ((u `1) * (z `2))) / (z `2) by A4, GROUP_1:def_3
.= (((v `2) * (u `1)) * (z `2)) / (z `2) by GROUP_1:def_3
.= ((v `2) * (u `1)) * ((z `2) / (z `2)) by A5, A9, GCD_1:11
.= ((u `1) * (v `2)) * (1_ I) by A9, GCD_1:9
.= (u `1) * (v `2) by VECTSP_1:def_4 ;
::_thesis: verum
end;
theorem Th8: :: QUOFIELD:8
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Quot. I st u meets v holds
u = v
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of Quot. I st u meets v holds
u = v
let u, v be Element of Quot. I; ::_thesis: ( u meets v implies u = v )
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
assume u /\ v <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: u = v
then u meets v by XBOOLE_0:def_7;
then consider w being set such that
A2: w in u and
A3: w in v by XBOOLE_0:3;
consider y being Element of Q. I such that
A4: v = QClass. y by Def5;
reconsider w = w as Element of Q. I by A2;
A5: (w `1) * (y `2) = (w `2) * (y `1) by A4, A3, Def4;
A6: for z being Element of Q. I st z in QClass. x holds
z in QClass. y
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. x implies z in QClass. y )
w `2 divides w `2 ;
then A7: w `2 divides ((z `2) * (y `1)) * (w `2) by GCD_1:7;
assume z in QClass. x ; ::_thesis: z in QClass. y
then A8: (z `1) * (w `2) = (z `2) * (w `1) by A1, A2, Th7;
then A9: w `2 divides (z `2) * (w `1) by GCD_1:def_1;
then A10: w `2 divides ((z `2) * (w `1)) * (y `2) by GCD_1:7;
A11: w `2 <> 0. I by Th2;
then (z `1) * (y `2) = (((z `2) * (w `1)) / (w `2)) * (y `2) by A8, A9, GCD_1:def_4
.= (((z `2) * (w `1)) * (y `2)) / (w `2) by A9, A10, A11, GCD_1:11
.= ((z `2) * ((w `2) * (y `1))) / (w `2) by A5, GROUP_1:def_3
.= (((z `2) * (y `1)) * (w `2)) / (w `2) by GROUP_1:def_3
.= ((z `2) * (y `1)) * ((w `2) / (w `2)) by A7, A11, GCD_1:11
.= ((z `2) * (y `1)) * (1_ I) by A11, GCD_1:9
.= (z `2) * (y `1) by VECTSP_1:def_4 ;
hence z in QClass. y by Def4; ::_thesis: verum
end;
A12: (w `1) * (x `2) = (w `2) * (x `1) by A1, A2, Def4;
for z being Element of Q. I st z in QClass. y holds
z in QClass. x
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. y implies z in QClass. x )
w `2 divides w `2 ;
then A13: w `2 divides ((z `2) * (x `1)) * (w `2) by GCD_1:7;
assume z in QClass. y ; ::_thesis: z in QClass. x
then A14: (z `1) * (w `2) = (z `2) * (w `1) by A4, A3, Th7;
then A15: w `2 divides (z `2) * (w `1) by GCD_1:def_1;
then A16: w `2 divides ((z `2) * (w `1)) * (x `2) by GCD_1:7;
A17: w `2 <> 0. I by Th2;
then (z `1) * (x `2) = (((z `2) * (w `1)) / (w `2)) * (x `2) by A14, A15, GCD_1:def_4
.= (((z `2) * (w `1)) * (x `2)) / (w `2) by A15, A16, A17, GCD_1:11
.= ((z `2) * ((w `2) * (x `1))) / (w `2) by A12, GROUP_1:def_3
.= (((z `2) * (x `1)) * (w `2)) / (w `2) by GROUP_1:def_3
.= ((z `2) * (x `1)) * ((w `2) / (w `2)) by A13, A17, GCD_1:11
.= ((z `2) * (x `1)) * (1_ I) by A17, GCD_1:9
.= (z `2) * (x `1) by VECTSP_1:def_4 ;
hence z in QClass. x by Def4; ::_thesis: verum
end;
hence u = v by A1, A4, A6, SUBSET_1:3; ::_thesis: verum
end;
begin
definition
let I be non degenerated commutative domRing-like Ring;
let u, v be Element of Quot. I;
func qadd (u,v) -> Element of Quot. I means :Def6: :: QUOFIELD:def 6
for z being Element of Q. I holds
( z in it iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) )
proof
consider y being Element of Q. I such that
A1: v = QClass. y by Def5;
consider x being Element of Q. I such that
A2: u = QClass. x by Def5;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then (x `2) * (y `2) <> 0. I by VECTSP_2:def_1;
then reconsider t = [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
XX: ( [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] `1 = ((x `1) * (y `2)) + ((y `1) * (x `2)) & [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
set M = QClass. t;
A3: for z being Element of Q. I st z in QClass. t holds
ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) )
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) )
assume z in QClass. t ; ::_thesis: ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (t `2) = (z `2) * (((x `1) * (y `2)) + ((y `1) * (x `2))) by XX;
then A4: (z `1) * ((x `2) * (y `2)) = (z `2) * (((x `1) * (y `2)) + ((y `1) * (x `2))) by XX;
x in u by A2, Th5;
hence ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) by A1, A4, Th5; ::_thesis: verum
end;
A5: for z being Element of Q. I st ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) implies z in QClass. t )
given a, b being Element of Q. I such that A6: a in u and
A7: b in v and
A8: (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ; ::_thesis: z in QClass. t
A9: (b `1) * (y `2) = (b `2) * (y `1) by A1, A7, Def4;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A10: (a `2) * (b `2) <> 0. I by VECTSP_2:def_1;
A11: (a `1) * (x `2) = (a `2) * (x `1) by A2, A6, Def4;
now__::_thesis:_(_(_((a_`1)_*_(b_`2))_+_((b_`1)_*_(a_`2))_=_0._I_&_z_in_QClass._t_)_or_(_((a_`1)_*_(b_`2))_+_((b_`1)_*_(a_`2))_<>_0._I_&_z_in_QClass._t_)_)
percases ( ((a `1) * (b `2)) + ((b `1) * (a `2)) = 0. I or ((a `1) * (b `2)) + ((b `1) * (a `2)) <> 0. I ) ;
caseA12: ((a `1) * (b `2)) + ((b `1) * (a `2)) = 0. I ; ::_thesis: z in QClass. t
then 0. I = (((a `1) * (b `2)) + ((b `1) * (a `2))) * ((x `2) * (y `2)) by VECTSP_1:7
.= ((((a `1) * (b `2)) + ((b `1) * (a `2))) * (x `2)) * (y `2) by GROUP_1:def_3
.= ((((a `1) * (b `2)) * (x `2)) + (((b `1) * (a `2)) * (x `2))) * (y `2) by VECTSP_1:def_3
.= ((((a `1) * (b `2)) * (x `2)) * (y `2)) + ((((b `1) * (a `2)) * (x `2)) * (y `2)) by VECTSP_1:def_3
.= ((((a `1) * (x `2)) * (b `2)) * (y `2)) + (((x `2) * ((a `2) * (b `1))) * (y `2)) by GROUP_1:def_3
.= ((((a `1) * (x `2)) * (b `2)) * (y `2)) + ((x `2) * (((a `2) * (b `1)) * (y `2))) by GROUP_1:def_3
.= ((((a `2) * (x `1)) * (b `2)) * (y `2)) + ((x `2) * ((a `2) * ((b `1) * (y `2)))) by A11, GROUP_1:def_3
.= ((((a `2) * (x `1)) * (b `2)) * (y `2)) + ((x `2) * (((a `2) * (b `2)) * (y `1))) by A9, GROUP_1:def_3
.= ((((a `2) * (x `1)) * (b `2)) * (y `2)) + (((x `2) * (y `1)) * ((a `2) * (b `2))) by GROUP_1:def_3
.= ((y `2) * ((x `1) * ((a `2) * (b `2)))) + (((x `2) * (y `1)) * ((a `2) * (b `2))) by GROUP_1:def_3
.= (((y `2) * (x `1)) * ((a `2) * (b `2))) + (((x `2) * (y `1)) * ((a `2) * (b `2))) by GROUP_1:def_3
.= (((y `2) * (x `1)) + ((x `2) * (y `1))) * ((a `2) * (b `2)) by VECTSP_1:def_3 ;
then A13: ((y `2) * (x `1)) + ((x `2) * (y `1)) = 0. I by A10, VECTSP_2:def_1;
(z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) = 0. I by A12, VECTSP_1:7;
then z `1 = 0. I by A8, A10, VECTSP_2:def_1;
then (z `1) * (t `2) = 0. I by VECTSP_1:7
.= (z `2) * (((y `2) * (x `1)) + ((x `2) * (y `1))) by A13, VECTSP_1:7
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
caseA14: ((a `1) * (b `2)) + ((b `1) * (a `2)) <> 0. I ; ::_thesis: z in QClass. t
((a `1) * (b `2)) + ((b `1) * (a `2)) divides ((a `1) * (b `2)) + ((b `1) * (a `2)) ;
then A15: ((a `1) * (b `2)) + ((b `1) * (a `2)) divides ((z `1) * ((y `2) * (x `2))) * (((a `1) * (b `2)) + ((b `1) * (a `2))) by GCD_1:7;
A16: ((z `1) * (((y `2) * (x `2)) * (((a `1) * (b `2)) + ((b `1) * (a `2))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) = (((z `1) * ((y `2) * (x `2))) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * ((y `2) * (x `2))) * ((((a `1) * (b `2)) + ((b `1) * (a `2))) / (((a `1) * (b `2)) + ((b `1) * (a `2)))) by A14, A15, GCD_1:11
.= ((z `1) * ((y `2) * (x `2))) * (1_ I) by A14, GCD_1:9
.= (z `1) * ((x `2) * (y `2)) by VECTSP_1:def_4 ;
A17: ((a `1) * (b `2)) + ((b `1) * (a `2)) divides (z `1) * ((a `2) * (b `2)) by A8, GCD_1:def_1;
then A18: ((a `1) * (b `2)) + ((b `1) * (a `2)) divides ((z `1) * ((a `2) * (b `2))) * (((x `1) * (y `2)) + ((y `1) * (x `2))) by GCD_1:7;
((z `1) * ((a `2) * (b `2))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) = z `2 by A8, A14, A17, GCD_1:def_4;
then (z `2) * (((x `1) * (y `2)) + ((y `1) * (x `2))) = (((z `1) * ((a `2) * (b `2))) * (((x `1) * (y `2)) + ((y `1) * (x `2)))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by A14, A17, A18, GCD_1:11
.= ((((z `1) * (a `2)) * (b `2)) * (((x `1) * (y `2)) + ((y `1) * (x `2)))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= (((z `1) * (a `2)) * ((b `2) * (((x `1) * (y `2)) + ((y `1) * (x `2))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * ((a `2) * ((b `2) * (((x `1) * (y `2)) + ((y `1) * (x `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * ((a `2) * (((b `2) * ((x `1) * (y `2))) + ((b `2) * ((y `1) * (x `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by VECTSP_1:def_2
.= ((z `1) * (((a `2) * ((b `2) * ((x `1) * (y `2)))) + ((a `2) * ((b `2) * ((y `1) * (x `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by VECTSP_1:def_2
.= ((z `1) * (((a `2) * (((b `2) * (x `1)) * (y `2))) + ((a `2) * ((b `2) * ((y `1) * (x `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * ((((a `2) * ((x `1) * (b `2))) * (y `2)) + ((a `2) * ((b `2) * ((y `1) * (x `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * (((((a `1) * (x `2)) * (b `2)) * (y `2)) + ((a `2) * ((b `2) * ((y `1) * (x `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by A11, GROUP_1:def_3
.= ((z `1) * (((((a `1) * (x `2)) * (b `2)) * (y `2)) + ((a `2) * (((b `1) * (y `2)) * (x `2))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by A9, GROUP_1:def_3
.= ((z `1) * (((y `2) * ((x `2) * ((a `1) * (b `2)))) + ((a `2) * (((b `1) * (y `2)) * (x `2))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * (((y `2) * ((x `2) * ((a `1) * (b `2)))) + ((x `2) * ((a `2) * ((b `1) * (y `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * (((y `2) * ((x `2) * ((a `1) * (b `2)))) + ((x `2) * ((y `2) * ((b `1) * (a `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * ((((y `2) * (x `2)) * ((a `1) * (b `2))) + ((x `2) * ((y `2) * ((b `1) * (a `2)))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * ((((y `2) * (x `2)) * ((a `1) * (b `2))) + (((y `2) * (x `2)) * ((b `1) * (a `2))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by GROUP_1:def_3
.= ((z `1) * (((y `2) * (x `2)) * (((a `1) * (b `2)) + ((b `1) * (a `2))))) / (((a `1) * (b `2)) + ((b `1) * (a `2))) by VECTSP_1:def_2 ;
then (z `1) * (t `2) = (z `2) * (((y `2) * (x `1)) + ((x `2) * (y `1))) by A16, XX
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
end;
end;
hence z in QClass. t ; ::_thesis: verum
end;
QClass. t is Element of Quot. I by Def5;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) by A5, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) holds
b1 = b2
proof
let M1, M2 be Element of Quot. I; ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) & ( for z being Element of Q. I holds
( z in M2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) implies M1 = M2 )
assume A19: for z being Element of Q. I holds
( z in M1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) implies ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) & not z in M2 ) ) or M1 = M2 )
assume A20: for z being Element of Q. I holds
( z in M2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ; ::_thesis: M1 = M2
A21: for x being set st x in M2 holds
x in M1
proof
let x be set ; ::_thesis: ( x in M2 implies x in M1 )
assume A22: x in M2 ; ::_thesis: x in M1
then reconsider x = x as Element of Q. I ;
ex a, b being Element of Q. I st
( a in u & b in v & (x `1) * ((a `2) * (b `2)) = (x `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) by A20, A22;
hence x in M1 by A19; ::_thesis: verum
end;
for x being set st x in M1 holds
x in M2
proof
let x be set ; ::_thesis: ( x in M1 implies x in M2 )
assume A23: x in M1 ; ::_thesis: x in M2
then reconsider x = x as Element of Q. I ;
ex a, b being Element of Q. I st
( a in u & b in v & (x `1) * ((a `2) * (b `2)) = (x `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) by A19, A23;
hence x in M2 by A20; ::_thesis: verum
end;
hence M1 = M2 by A21, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines qadd QUOFIELD:def_6_:_
for I being non degenerated commutative domRing-like Ring
for u, v, b4 being Element of Quot. I holds
( b4 = qadd (u,v) iff for z being Element of Q. I holds
( z in b4 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) );
definition
let I be non degenerated commutative domRing-like Ring;
let u, v be Element of Quot. I;
func qmult (u,v) -> Element of Quot. I means :Def7: :: QUOFIELD:def 7
for z being Element of Q. I holds
( z in it iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) )
proof
consider y being Element of Q. I such that
A1: v = QClass. y by Def5;
consider x being Element of Q. I such that
A2: u = QClass. x by Def5;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then (x `2) * (y `2) <> 0. I by VECTSP_2:def_1;
then reconsider t = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
XX: ( [((x `1) * (y `1)),((x `2) * (y `2))] `1 = (x `1) * (y `1) & [((x `1) * (y `1)),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
set M = QClass. t;
A3: for z being Element of Q. I st z in QClass. t holds
ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) )
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) )
assume z in QClass. t ; ::_thesis: ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (t `2) = (z `2) * ((x `1) * (y `1)) by XX;
then A4: (z `1) * ((x `2) * (y `2)) = (z `2) * ((x `1) * (y `1)) by XX;
x in u by A2, Th5;
hence ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) by A1, A4, Th5; ::_thesis: verum
end;
A5: for z being Element of Q. I st ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) implies z in QClass. t )
given a, b being Element of Q. I such that A6: a in u and
A7: b in v and
A8: (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ; ::_thesis: z in QClass. t
A9: (a `1) * (x `2) = (a `2) * (x `1) by A2, A6, Def4;
A10: (b `1) * (y `2) = (b `2) * (y `1) by A1, A7, Def4;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A11: (a `2) * (b `2) <> 0. I by VECTSP_2:def_1;
A12: (a `2) * (b `2) divides (z `2) * ((a `1) * (b `1)) by A8, GCD_1:def_1;
then A13: (a `2) * (b `2) divides ((z `2) * ((a `1) * (b `1))) * ((x `2) * (y `2)) by GCD_1:7;
(a `2) * (b `2) divides (a `2) * (b `2) ;
then (a `2) * (b `2) divides ((z `2) * ((x `1) * (y `1))) * ((a `2) * (b `2)) by GCD_1:7;
then A14: (((z `2) * ((x `1) * (y `1))) * ((a `2) * (b `2))) / ((a `2) * (b `2)) = ((z `2) * ((x `1) * (y `1))) * (((a `2) * (b `2)) / ((a `2) * (b `2))) by A11, GCD_1:11
.= ((z `2) * ((x `1) * (y `1))) * (1_ I) by A11, GCD_1:9
.= (z `2) * ((x `1) * (y `1)) by VECTSP_1:def_4 ;
((z `2) * ((a `1) * (b `1))) / ((a `2) * (b `2)) = z `1 by A8, A12, A11, GCD_1:def_4;
then (z `1) * ((x `2) * (y `2)) = (((z `2) * ((a `1) * (b `1))) * ((x `2) * (y `2))) / ((a `2) * (b `2)) by A12, A11, A13, GCD_1:11
.= ((z `2) * (((a `1) * (b `1)) * ((x `2) * (y `2)))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((a `1) * ((b `1) * ((x `2) * (y `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((a `1) * ((x `2) * ((b `1) * (y `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * (((a `2) * (x `1)) * ((b `1) * (y `2)))) / ((a `2) * (b `2)) by A9, GROUP_1:def_3
.= ((z `2) * ((x `1) * ((a `2) * ((b `2) * (y `1))))) / ((a `2) * (b `2)) by A10, GROUP_1:def_3
.= ((z `2) * ((x `1) * ((y `1) * ((a `2) * (b `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * (((x `1) * (y `1)) * ((a `2) * (b `2)))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= (((z `2) * ((x `1) * (y `1))) * ((a `2) * (b `2))) / ((a `2) * (b `2)) by GROUP_1:def_3 ;
then (z `1) * (t `2) = (z `2) * ((x `1) * (y `1)) by A14, XX
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
QClass. t is Element of Quot. I by Def5;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) by A5, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ) holds
b1 = b2
proof
let M1, M2 be Element of Quot. I; ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ) & ( for z being Element of Q. I holds
( z in M2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ) implies M1 = M2 )
assume A15: for z being Element of Q. I holds
( z in M1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) implies ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) & not z in M2 ) ) or M1 = M2 )
assume A16: for z being Element of Q. I holds
( z in M2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ; ::_thesis: M1 = M2
A17: for x being set st x in M2 holds
x in M1
proof
let x be set ; ::_thesis: ( x in M2 implies x in M1 )
assume A18: x in M2 ; ::_thesis: x in M1
then reconsider x = x as Element of Q. I ;
ex a, b being Element of Q. I st
( a in u & b in v & (x `1) * ((a `2) * (b `2)) = (x `2) * ((a `1) * (b `1)) ) by A16, A18;
hence x in M1 by A15; ::_thesis: verum
end;
for x being set st x in M1 holds
x in M2
proof
let x be set ; ::_thesis: ( x in M1 implies x in M2 )
assume A19: x in M1 ; ::_thesis: x in M2
then reconsider x = x as Element of Q. I ;
ex a, b being Element of Q. I st
( a in u & b in v & (x `1) * ((a `2) * (b `2)) = (x `2) * ((a `1) * (b `1)) ) by A15, A19;
hence x in M2 by A16; ::_thesis: verum
end;
hence M1 = M2 by A17, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines qmult QUOFIELD:def_7_:_
for I being non degenerated commutative domRing-like Ring
for u, v, b4 being Element of Quot. I holds
( b4 = qmult (u,v) iff for z being Element of Q. I holds
( z in b4 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) );
definition
let I be non empty non degenerated multLoopStr_0 ;
let u be Element of Q. I;
:: original: QClass.
redefine func QClass. u -> Element of Quot. I;
coherence
QClass. u is Element of Quot. I by Def5;
end;
theorem Th9: :: QUOFIELD:9
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Q. I holds qadd ((QClass. u),(QClass. v)) = QClass. (padd (u,v))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of Q. I holds qadd ((QClass. u),(QClass. v)) = QClass. (padd (u,v))
let u, v be Element of Q. I; ::_thesis: qadd ((QClass. u),(QClass. v)) = QClass. (padd (u,v))
( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then (u `2) * (v `2) <> 0. I by VECTSP_2:def_1;
then reconsider w = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] as Element of Q. I by Def1;
XX: ( [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] `1 = ((u `1) * (v `2)) + ((v `1) * (u `2)) & [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
A1: ( w `1 = ((u `1) * (v `2)) + ((v `1) * (u `2)) & w `2 = (u `2) * (v `2) ) by XX;
A2: for z being Element of Q. I st z in qadd ((QClass. u),(QClass. v)) holds
z in QClass. (padd (u,v))
proof
let z be Element of Q. I; ::_thesis: ( z in qadd ((QClass. u),(QClass. v)) implies z in QClass. (padd (u,v)) )
assume z in qadd ((QClass. u),(QClass. v)) ; ::_thesis: z in QClass. (padd (u,v))
then consider a, b being Element of Q. I such that
A3: a in QClass. u and
A4: b in QClass. v and
A5: (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) by Def6;
A6: (a `1) * (u `2) = (a `2) * (u `1) by A3, Def4;
A7: (b `1) * (v `2) = (b `2) * (v `1) by A4, Def4;
(a `2) * (b `2) divides (a `2) * (b `2) ;
then A8: (a `2) * (b `2) divides ((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * ((a `2) * (b `2)) by GCD_1:7;
A9: (a `2) * (b `2) divides (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) by A5, GCD_1:def_1;
then A10: (a `2) * (b `2) divides ((z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) * ((u `2) * (v `2)) by GCD_1:7;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A11: (a `2) * (b `2) <> 0. I by VECTSP_2:def_1;
then z `1 = ((z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) / ((a `2) * (b `2)) by A5, A9, GCD_1:def_4;
then (z `1) * ((u `2) * (v `2)) = (((z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) * ((u `2) * (v `2))) / ((a `2) * (b `2)) by A11, A9, A10, GCD_1:11
.= ((z `2) * ((((a `1) * (b `2)) + ((b `1) * (a `2))) * ((u `2) * (v `2)))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((a `1) * (b `2)) * ((u `2) * (v `2))) + (((b `1) * (a `2)) * ((u `2) * (v `2))))) / ((a `2) * (b `2)) by VECTSP_1:def_3
.= ((z `2) * (((b `2) * ((a `1) * ((u `2) * (v `2)))) + (((b `1) * (a `2)) * ((u `2) * (v `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * (((b `2) * (((a `2) * (u `1)) * (v `2))) + (((b `1) * (a `2)) * ((u `2) * (v `2))))) / ((a `2) * (b `2)) by A6, GROUP_1:def_3
.= ((z `2) * (((b `2) * (((a `2) * (u `1)) * (v `2))) + ((a `2) * ((b `1) * ((v `2) * (u `2)))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * (((b `2) * (((a `2) * (u `1)) * (v `2))) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by A7, GROUP_1:def_3
.= ((z `2) * ((((b `2) * ((a `2) * (u `1))) * (v `2)) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((u `1) * ((b `2) * (a `2))) * (v `2)) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((u `1) * (v `2)) * ((b `2) * (a `2))) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((u `1) * (v `2)) * ((b `2) * (a `2))) + (((a `2) * ((b `2) * (v `1))) * (u `2)))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((u `1) * (v `2)) * ((a `2) * (b `2))) + (((v `1) * ((a `2) * (b `2))) * (u `2)))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((u `1) * (v `2)) * ((a `2) * (b `2))) + (((v `1) * (u `2)) * ((a `2) * (b `2))))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * ((((u `1) * (v `2)) + ((v `1) * (u `2))) * ((a `2) * (b `2)))) / ((a `2) * (b `2)) by VECTSP_1:def_3
.= (((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * ((a `2) * (b `2))) / ((a `2) * (b `2)) by GROUP_1:def_3
.= ((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * (((a `2) * (b `2)) / ((a `2) * (b `2))) by A11, A8, GCD_1:11
.= ((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * (1_ I) by A11, GCD_1:9
.= (z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2))) by VECTSP_1:def_4 ;
hence z in QClass. (padd (u,v)) by A1, Def4; ::_thesis: verum
end;
for z being Element of Q. I st z in QClass. (padd (u,v)) holds
z in qadd ((QClass. u),(QClass. v))
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. (padd (u,v)) implies z in qadd ((QClass. u),(QClass. v)) )
assume z in QClass. (padd (u,v)) ; ::_thesis: z in qadd ((QClass. u),(QClass. v))
then A12: (z `1) * ((u `2) * (v `2)) = (z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2))) by A1, Def4;
( u in QClass. u & v in QClass. v ) by Th5;
hence z in qadd ((QClass. u),(QClass. v)) by A12, Def6; ::_thesis: verum
end;
hence qadd ((QClass. u),(QClass. v)) = QClass. (padd (u,v)) by A2, SUBSET_1:3; ::_thesis: verum
end;
theorem Th10: :: QUOFIELD:10
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Q. I holds qmult ((QClass. u),(QClass. v)) = QClass. (pmult (u,v))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of Q. I holds qmult ((QClass. u),(QClass. v)) = QClass. (pmult (u,v))
let u, v be Element of Q. I; ::_thesis: qmult ((QClass. u),(QClass. v)) = QClass. (pmult (u,v))
( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then (u `2) * (v `2) <> 0. I by VECTSP_2:def_1;
then reconsider w = [((u `1) * (v `1)),((u `2) * (v `2))] as Element of Q. I by Def1;
( [((u `1) * (v `1)),((u `2) * (v `2))] `1 = (u `1) * (v `1) & [((u `1) * (v `1)),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
then A1: ( w `1 = (u `1) * (v `1) & w `2 = (u `2) * (v `2) ) ;
A2: for z being Element of Q. I st z in qmult ((QClass. u),(QClass. v)) holds
z in QClass. (pmult (u,v))
proof
let z be Element of Q. I; ::_thesis: ( z in qmult ((QClass. u),(QClass. v)) implies z in QClass. (pmult (u,v)) )
assume z in qmult ((QClass. u),(QClass. v)) ; ::_thesis: z in QClass. (pmult (u,v))
then consider a, b being Element of Q. I such that
A3: a in QClass. u and
A4: b in QClass. v and
A5: (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) by Def7;
A6: (b `1) * (v `2) = (b `2) * (v `1) by A4, Def4;
A7: (a `1) * (u `2) = (a `2) * (u `1) by A3, Def4;
now__::_thesis:_(_(_a_`1_=_0._I_&_z_in_QClass._(pmult_(u,v))_)_or_(_b_`1_=_0._I_&_z_in_QClass._(pmult_(u,v))_)_or_(_a_`1_<>_0._I_&_b_`1_<>_0._I_&_z_in_QClass._(pmult_(u,v))_)_)
percases ( a `1 = 0. I or b `1 = 0. I or ( a `1 <> 0. I & b `1 <> 0. I ) ) ;
caseA8: a `1 = 0. I ; ::_thesis: z in QClass. (pmult (u,v))
then (a `1) * (b `1) = 0. I by VECTSP_1:7;
then A9: (z `2) * ((a `1) * (b `1)) = 0. I by VECTSP_1:7;
A10: a `2 <> 0. I by Th2;
b `2 <> 0. I by Th2;
then (a `2) * (b `2) <> 0. I by A10, VECTSP_2:def_1;
then A11: z `1 = 0. I by A5, A9, VECTSP_2:def_1;
(a `1) * (u `2) = 0. I by A8, VECTSP_1:7;
then u `1 = 0. I by A7, A10, VECTSP_2:def_1;
then (z `2) * ((u `1) * (v `1)) = (z `2) * (0. I) by VECTSP_1:7
.= 0. I by VECTSP_1:7
.= (z `1) * ((u `2) * (v `2)) by A11, VECTSP_1:7 ;
hence z in QClass. (pmult (u,v)) by A1, Def4; ::_thesis: verum
end;
caseA12: b `1 = 0. I ; ::_thesis: z in QClass. (pmult (u,v))
then (a `1) * (b `1) = 0. I by VECTSP_1:7;
then A13: (z `2) * ((a `1) * (b `1)) = 0. I by VECTSP_1:7;
A14: b `2 <> 0. I by Th2;
a `2 <> 0. I by Th2;
then (a `2) * (b `2) <> 0. I by A14, VECTSP_2:def_1;
then A15: z `1 = 0. I by A5, A13, VECTSP_2:def_1;
(b `1) * (v `2) = 0. I by A12, VECTSP_1:7;
then v `1 = 0. I by A6, A14, VECTSP_2:def_1;
then (z `2) * ((u `1) * (v `1)) = (z `2) * (0. I) by VECTSP_1:7
.= 0. I by VECTSP_1:7
.= (z `1) * ((u `2) * (v `2)) by A15, VECTSP_1:7 ;
hence z in QClass. (pmult (u,v)) by A1, Def4; ::_thesis: verum
end;
caseA16: ( a `1 <> 0. I & b `1 <> 0. I ) ; ::_thesis: z in QClass. (pmult (u,v))
(a `1) * (b `1) divides (a `1) * (b `1) ;
then A17: (a `1) * (b `1) divides (((z `2) * (u `1)) * (v `1)) * ((a `1) * (b `1)) by GCD_1:7;
A18: (a `1) * (b `1) <> 0. I by A16, VECTSP_2:def_1;
A19: b `1 divides (b `2) * (v `1) by A6, GCD_1:def_1;
then A20: v `2 = ((b `2) * (v `1)) / (b `1) by A6, A16, GCD_1:def_4;
A21: a `1 divides (a `2) * (u `1) by A7, GCD_1:def_1;
then A22: (a `1) * (b `1) divides ((a `2) * (u `1)) * ((b `2) * (v `1)) by A19, GCD_1:3;
then A23: (a `1) * (b `1) divides (z `1) * (((a `2) * (u `1)) * ((b `2) * (v `1))) by GCD_1:7;
u `2 = ((a `2) * (u `1)) / (a `1) by A7, A16, A21, GCD_1:def_4;
then (z `1) * ((u `2) * (v `2)) = (z `1) * ((((a `2) * (u `1)) * ((b `2) * (v `1))) / ((a `1) * (b `1))) by A16, A21, A19, A20, GCD_1:14
.= ((z `1) * (((a `2) * (u `1)) * ((b `2) * (v `1)))) / ((a `1) * (b `1)) by A18, A22, A23, GCD_1:11
.= ((z `1) * ((((u `1) * (a `2)) * (b `2)) * (v `1))) / ((a `1) * (b `1)) by GROUP_1:def_3
.= ((z `1) * ((((a `2) * (b `2)) * (u `1)) * (v `1))) / ((a `1) * (b `1)) by GROUP_1:def_3
.= (((z `1) * (((a `2) * (b `2)) * (u `1))) * (v `1)) / ((a `1) * (b `1)) by GROUP_1:def_3
.= ((((z `2) * ((a `1) * (b `1))) * (u `1)) * (v `1)) / ((a `1) * (b `1)) by A5, GROUP_1:def_3
.= ((((z `2) * (u `1)) * ((a `1) * (b `1))) * (v `1)) / ((a `1) * (b `1)) by GROUP_1:def_3
.= ((((z `2) * (u `1)) * (v `1)) * ((a `1) * (b `1))) / ((a `1) * (b `1)) by GROUP_1:def_3
.= (((z `2) * (u `1)) * (v `1)) * (((a `1) * (b `1)) / ((a `1) * (b `1))) by A18, A17, GCD_1:11
.= (((z `2) * (u `1)) * (v `1)) * (1_ I) by A18, GCD_1:9
.= ((z `2) * (u `1)) * (v `1) by VECTSP_1:def_4
.= (z `2) * ((u `1) * (v `1)) by GROUP_1:def_3 ;
hence z in QClass. (pmult (u,v)) by A1, Def4; ::_thesis: verum
end;
end;
end;
hence z in QClass. (pmult (u,v)) ; ::_thesis: verum
end;
for z being Element of Q. I st z in QClass. (pmult (u,v)) holds
z in qmult ((QClass. u),(QClass. v))
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. (pmult (u,v)) implies z in qmult ((QClass. u),(QClass. v)) )
assume z in QClass. (pmult (u,v)) ; ::_thesis: z in qmult ((QClass. u),(QClass. v))
then A24: (z `1) * ((u `2) * (v `2)) = (z `2) * ((u `1) * (v `1)) by A1, Def4;
( u in QClass. u & v in QClass. v ) by Th5;
hence z in qmult ((QClass. u),(QClass. v)) by A24, Def7; ::_thesis: verum
end;
hence qmult ((QClass. u),(QClass. v)) = QClass. (pmult (u,v)) by A2, SUBSET_1:3; ::_thesis: verum
end;
definition
let I be non degenerated commutative domRing-like Ring;
func q0. I -> Element of Quot. I means :Def8: :: QUOFIELD:def 8
for z being Element of Q. I holds
( z in it iff z `1 = 0. I );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I )
proof
reconsider t = [(0. I),(1_ I)] as Element of Q. I by Def1;
XX: ( [(0. I),(1_ I)] `1 = 0. I & [(0. I),(1_ I)] `2 = 1_ I ) ;
set M = QClass. t;
A1: for z being Element of Q. I st z in QClass. t holds
z `1 = 0. I
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies z `1 = 0. I )
assume z in QClass. t ; ::_thesis: z `1 = 0. I
then A2: (z `1) * (t `2) = (z `2) * (t `1) by Def4
.= (z `2) * (0. I) by XX
.= 0. I by VECTSP_1:7 ;
t `2 <> 0. I by Th2;
hence z `1 = 0. I by A2, VECTSP_2:def_1; ::_thesis: verum
end;
for z being Element of Q. I st z `1 = 0. I holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( z `1 = 0. I implies z in QClass. t )
assume z `1 = 0. I ; ::_thesis: z in QClass. t
then (z `1) * (t `2) = 0. I by VECTSP_1:7
.= (z `2) * (0. I) by VECTSP_1:7
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds
( z in b2 iff z `1 = 0. I ) ) holds
b1 = b2
proof
let M1, M2 be Element of Quot. I; ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds
( z in M2 iff z `1 = 0. I ) ) implies M1 = M2 )
assume A3: for z being Element of Q. I holds
( z in M1 iff z `1 = 0. I ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies z `1 = 0. I ) implies ( z `1 = 0. I & not z in M2 ) ) or M1 = M2 )
assume A4: for z being Element of Q. I holds
( z in M2 iff z `1 = 0. I ) ; ::_thesis: M1 = M2
A5: for z being Element of Q. I st z in M2 holds
z in M1
proof
let z be Element of Q. I; ::_thesis: ( z in M2 implies z in M1 )
assume z in M2 ; ::_thesis: z in M1
then z `1 = 0. I by A4;
hence z in M1 by A3; ::_thesis: verum
end;
for z being Element of Q. I st z in M1 holds
z in M2
proof
let z be Element of Q. I; ::_thesis: ( z in M1 implies z in M2 )
assume z in M1 ; ::_thesis: z in M2
then z `1 = 0. I by A3;
hence z in M2 by A4; ::_thesis: verum
end;
hence M1 = M2 by A5, SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines q0. QUOFIELD:def_8_:_
for I being non degenerated commutative domRing-like Ring
for b2 being Element of Quot. I holds
( b2 = q0. I iff for z being Element of Q. I holds
( z in b2 iff z `1 = 0. I ) );
definition
let I be non degenerated commutative domRing-like Ring;
func q1. I -> Element of Quot. I means :Def9: :: QUOFIELD:def 9
for z being Element of Q. I holds
( z in it iff z `1 = z `2 );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = z `2 )
proof
1_ I <> 0. I ;
then reconsider t = [(1_ I),(1_ I)] as Element of Q. I by Def1;
XX: ( [(1_ I),(1_ I)] `1 = 1_ I & [(1_ I),(1_ I)] `2 = 1_ I ) ;
set M = QClass. t;
A1: for z being Element of Q. I st z in QClass. t holds
z `1 = z `2
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies z `1 = z `2 )
assume z in QClass. t ; ::_thesis: z `1 = z `2
then A2: (z `1) * (t `2) = (z `2) * (t `1) by Def4;
z `1 = (z `1) * (1_ I) by VECTSP_1:def_4
.= (z `2) * (t `1) by A2, XX
.= (z `2) * (1_ I) by XX
.= z `2 by VECTSP_1:def_4 ;
hence z `1 = z `2 ; ::_thesis: verum
end;
for z being Element of Q. I st z `1 = z `2 holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( z `1 = z `2 implies z in QClass. t )
assume z `1 = z `2 ; ::_thesis: z in QClass. t
then (z `1) * (t `2) = (z `2) * (1_ I) by XX
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = z `2 ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff z `1 = z `2 ) ) & ( for z being Element of Q. I holds
( z in b2 iff z `1 = z `2 ) ) holds
b1 = b2
proof
let M1, M2 be Element of Quot. I; ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff z `1 = z `2 ) ) & ( for z being Element of Q. I holds
( z in M2 iff z `1 = z `2 ) ) implies M1 = M2 )
assume A3: for z being Element of Q. I holds
( z in M1 iff z `1 = z `2 ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies z `1 = z `2 ) implies ( z `1 = z `2 & not z in M2 ) ) or M1 = M2 )
assume A4: for z being Element of Q. I holds
( z in M2 iff z `1 = z `2 ) ; ::_thesis: M1 = M2
A5: for z being Element of Q. I st z in M2 holds
z in M1
proof
let z be Element of Q. I; ::_thesis: ( z in M2 implies z in M1 )
assume z in M2 ; ::_thesis: z in M1
then z `1 = z `2 by A4;
hence z in M1 by A3; ::_thesis: verum
end;
for z being Element of Q. I st z in M1 holds
z in M2
proof
let z be Element of Q. I; ::_thesis: ( z in M1 implies z in M2 )
assume z in M1 ; ::_thesis: z in M2
then z `1 = z `2 by A3;
hence z in M2 by A4; ::_thesis: verum
end;
hence M1 = M2 by A5, SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines q1. QUOFIELD:def_9_:_
for I being non degenerated commutative domRing-like Ring
for b2 being Element of Quot. I holds
( b2 = q1. I iff for z being Element of Q. I holds
( z in b2 iff z `1 = z `2 ) );
definition
let I be non degenerated commutative domRing-like Ring;
let u be Element of Quot. I;
func qaddinv u -> Element of Quot. I means :Def10: :: QUOFIELD:def 10
for z being Element of Q. I holds
( z in it iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )
proof
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
x `2 <> 0. I by Th2;
then reconsider t = [(- (x `1)),(x `2)] as Element of Q. I by Def1;
XX: ( [(- (x `1)),(x `2)] `1 = - (x `1) & [(- (x `1)),(x `2)] `2 = x `2 ) ;
set M = QClass. t;
A2: for z being Element of Q. I st ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) implies z in QClass. t )
given a being Element of Q. I such that A3: a in u and
A4: (z `1) * (a `2) = (z `2) * (- (a `1)) ; ::_thesis: z in QClass. t
A5: (a `1) * (x `2) = (a `2) * (x `1) by A1, A3, Def4;
A6: ((z `1) * (x `2)) * (a `2) = ((z `2) * (- (a `1))) * (x `2) by A4, GROUP_1:def_3
.= (- ((z `2) * (a `1))) * (x `2) by GCD_1:48
.= ((- (z `2)) * (a `1)) * (x `2) by GCD_1:48
.= (- (z `2)) * ((a `2) * (x `1)) by A5, GROUP_1:def_3
.= ((- (z `2)) * (x `1)) * (a `2) by GROUP_1:def_3
.= (- ((z `2) * (x `1))) * (a `2) by GCD_1:48
.= ((z `2) * (- (x `1))) * (a `2) by GCD_1:48 ;
A7: a `2 <> 0. I by Th2;
a `2 divides a `2 ;
then A8: a `2 divides ((z `2) * (- (x `1))) * (a `2) by GCD_1:7;
a `2 divides a `2 ;
then A9: a `2 divides ((z `1) * (x `2)) * (a `2) by GCD_1:7;
(z `1) * (t `2) = (z `1) * (x `2) by XX
.= ((z `1) * (x `2)) * (1_ I) by VECTSP_1:def_4
.= ((z `1) * (x `2)) * ((a `2) / (a `2)) by A7, GCD_1:9
.= (((z `2) * (- (x `1))) * (a `2)) / (a `2) by A7, A6, A9, GCD_1:11
.= ((z `2) * (- (x `1))) * ((a `2) / (a `2)) by A7, A8, GCD_1:11
.= ((z `2) * (- (x `1))) * (1_ I) by A7, GCD_1:9
.= (z `2) * (- (x `1)) by VECTSP_1:def_4
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
for z being Element of Q. I st z in QClass. t holds
ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) )
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )
assume z in QClass. t ; ::_thesis: ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (x `2) = (z `2) * (t `1) by XX
.= (z `2) * (- (x `1)) by XX ;
hence ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) by A1, Th5; ::_thesis: verum
end;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) holds
b1 = b2
proof
let M1, M2 be Element of Quot. I; ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) & ( for z being Element of Q. I holds
( z in M2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) implies M1 = M2 )
assume A10: for z being Element of Q. I holds
( z in M1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) implies ( ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) & not z in M2 ) ) or M1 = M2 )
assume A11: for z being Element of Q. I holds
( z in M2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ; ::_thesis: M1 = M2
A12: for z being Element of Q. I st z in M2 holds
z in M1
proof
let z be Element of Q. I; ::_thesis: ( z in M2 implies z in M1 )
assume z in M2 ; ::_thesis: z in M1
then ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) by A11;
hence z in M1 by A10; ::_thesis: verum
end;
for z being Element of Q. I st z in M1 holds
z in M2
proof
let z be Element of Q. I; ::_thesis: ( z in M1 implies z in M2 )
assume z in M1 ; ::_thesis: z in M2
then ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) by A10;
hence z in M2 by A11; ::_thesis: verum
end;
hence M1 = M2 by A12, SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines qaddinv QUOFIELD:def_10_:_
for I being non degenerated commutative domRing-like Ring
for u, b3 being Element of Quot. I holds
( b3 = qaddinv u iff for z being Element of Q. I holds
( z in b3 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) );
definition
let I be non degenerated commutative domRing-like Ring;
let u be Element of Quot. I;
assume A1: u <> q0. I ;
func qmultinv u -> Element of Quot. I means :Def11: :: QUOFIELD:def 11
for z being Element of Q. I holds
( z in it iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) )
proof
consider x being Element of Q. I such that
A2: u = QClass. x by Def5;
x `1 <> 0. I
proof
assume x `1 = 0. I ; ::_thesis: contradiction
then A3: x in q0. I by Def8;
x in u by A2, Th5;
then u meets q0. I by A3, XBOOLE_0:3;
hence contradiction by A1, Th8; ::_thesis: verum
end;
then reconsider t = [(x `2),(x `1)] as Element of Q. I by Def1;
XX: ( [(x `2),(x `1)] `1 = x `2 & [(x `2),(x `1)] `2 = x `1 ) ;
set M = QClass. t;
A4: for z being Element of Q. I st ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) implies z in QClass. t )
given a being Element of Q. I such that A5: a in u and
A6: (z `1) * (a `1) = (z `2) * (a `2) ; ::_thesis: z in QClass. t
A7: (a `1) * (x `2) = (a `2) * (x `1) by A2, A5, Def4;
A8: ((z `1) * (t `2)) * (a `2) = ((z `1) * (x `1)) * (a `2) by XX
.= (z `1) * ((a `1) * (x `2)) by A7, GROUP_1:def_3
.= ((z `2) * (a `2)) * (x `2) by A6, GROUP_1:def_3
.= ((z `2) * (a `2)) * (t `1) by XX
.= ((z `2) * (t `1)) * (a `2) by GROUP_1:def_3 ;
A9: a `2 <> 0. I by Th2;
a `2 divides a `2 ;
then A10: a `2 divides ((z `2) * (t `1)) * (a `2) by GCD_1:7;
a `2 divides a `2 ;
then A11: a `2 divides ((z `1) * (t `2)) * (a `2) by GCD_1:7;
(z `1) * (t `2) = ((z `1) * (t `2)) * (1_ I) by VECTSP_1:def_4
.= ((z `1) * (t `2)) * ((a `2) / (a `2)) by A9, GCD_1:9
.= (((z `2) * (t `1)) * (a `2)) / (a `2) by A9, A8, A11, GCD_1:11
.= ((z `2) * (t `1)) * ((a `2) / (a `2)) by A9, A10, GCD_1:11
.= ((z `2) * (t `1)) * (1_ I) by A9, GCD_1:9
.= (z `2) * (t `1) by VECTSP_1:def_4 ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
for z being Element of Q. I st z in QClass. t holds
ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) )
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) )
assume z in QClass. t ; ::_thesis: ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (x `1) = (z `2) * (t `1) by XX
.= (z `2) * (x `2) by XX ;
hence ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) by A2, Th5; ::_thesis: verum
end;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) holds
b1 = b2
proof
let M1, M2 be Element of Quot. I; ::_thesis: ( ( for z being Element of Q. I holds
( z in M1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) & ( for z being Element of Q. I holds
( z in M2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) implies M1 = M2 )
assume A12: for z being Element of Q. I holds
( z in M1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ; ::_thesis: ( ex z being Element of Q. I st
( ( z in M2 implies ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) implies ( ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) & not z in M2 ) ) or M1 = M2 )
assume A13: for z being Element of Q. I holds
( z in M2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ; ::_thesis: M1 = M2
A14: for z being Element of Q. I st z in M2 holds
z in M1
proof
let z be Element of Q. I; ::_thesis: ( z in M2 implies z in M1 )
assume z in M2 ; ::_thesis: z in M1
then ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) by A13;
hence z in M1 by A12; ::_thesis: verum
end;
for z being Element of Q. I st z in M1 holds
z in M2
proof
let z be Element of Q. I; ::_thesis: ( z in M1 implies z in M2 )
assume z in M1 ; ::_thesis: z in M2
then ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) by A12;
hence z in M2 by A13; ::_thesis: verum
end;
hence M1 = M2 by A14, SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines qmultinv QUOFIELD:def_11_:_
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I st u <> q0. I holds
for b3 being Element of Quot. I holds
( b3 = qmultinv u iff for z being Element of Q. I holds
( z in b3 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) );
theorem Th11: :: QUOFIELD:11
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds
( qadd (u,(qadd (v,w))) = qadd ((qadd (u,v)),w) & qadd (u,v) = qadd (v,u) )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds
( qadd (u,(qadd (v,w))) = qadd ((qadd (u,v)),w) & qadd (u,v) = qadd (v,u) )
let u, v, w be Element of Quot. I; ::_thesis: ( qadd (u,(qadd (v,w))) = qadd ((qadd (u,v)),w) & qadd (u,v) = qadd (v,u) )
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
consider z being Element of Q. I such that
A2: w = QClass. z by Def5;
consider y being Element of Q. I such that
A3: v = QClass. y by Def5;
A4: qadd (u,v) = QClass. (padd (x,y)) by A1, A3, Th9
.= qadd (v,u) by A1, A3, Th9 ;
qadd (u,(qadd (v,w))) = qadd ((QClass. x),(QClass. (padd (y,z)))) by A1, A3, A2, Th9
.= QClass. (padd (x,(padd (y,z)))) by Th9
.= QClass. (padd ((padd (x,y)),z)) by Th3
.= qadd ((QClass. (padd (x,y))),(QClass. z)) by Th9
.= qadd ((qadd (u,v)),w) by A1, A3, A2, Th9 ;
hence ( qadd (u,(qadd (v,w))) = qadd ((qadd (u,v)),w) & qadd (u,v) = qadd (v,u) ) by A4; ::_thesis: verum
end;
theorem Th12: :: QUOFIELD:12
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I holds
( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u )
let u be Element of Quot. I; ::_thesis: ( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u )
consider x being Element of Q. I such that
A1: q0. I = QClass. x by Def5;
consider y being Element of Q. I such that
A2: u = QClass. y by Def5;
A3: x `2 <> 0. I by Th2;
y `2 <> 0. I by Th2;
then (x `2) * (y `2) <> 0. I by A3, VECTSP_2:def_1;
then reconsider t = [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
XX: ( [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] `1 = ((y `1) * (x `2)) + ((x `1) * (y `2)) & [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
x in q0. I by A1, Th5;
then A4: x `1 = 0. I by Def8;
A5: for z being Element of Q. I st z in QClass. y holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. y implies z in QClass. t )
assume z in QClass. y ; ::_thesis: z in QClass. t
then A6: (z `1) * (y `2) = (z `2) * (y `1) by Def4;
(z `1) * (t `2) = (z `1) * ((x `2) * (y `2)) by XX
.= ((z `2) * (y `1)) * (x `2) by A6, GROUP_1:def_3
.= (z `2) * ((y `1) * (x `2)) by GROUP_1:def_3
.= (z `2) * (((y `1) * (x `2)) + (0. I)) by RLVECT_1:4
.= (z `2) * (((y `1) * (x `2)) + ((x `1) * (y `2))) by A4, VECTSP_1:7
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
A7: for z being Element of Q. I st z in QClass. t holds
z in QClass. y
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies z in QClass. y )
x `2 divides x `2 ;
then A8: x `2 divides ((z `1) * (y `2)) * (x `2) by GCD_1:7;
x `2 divides x `2 ;
then A9: x `2 divides ((z `2) * (y `1)) * (x `2) by GCD_1:7;
assume z in QClass. t ; ::_thesis: z in QClass. y
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then A10: (z `1) * ((x `2) * (y `2)) = (z `2) * (t `1) by XX;
A11: ((z `1) * (y `2)) * (x `2) = (z `1) * ((x `2) * (y `2)) by GROUP_1:def_3
.= (z `2) * (((y `1) * (x `2)) + ((0. I) * (y `2))) by A4, A10, XX
.= (z `2) * (((y `1) * (x `2)) + (0. I)) by VECTSP_1:7
.= (z `2) * ((y `1) * (x `2)) by RLVECT_1:4
.= ((z `2) * (y `1)) * (x `2) by GROUP_1:def_3 ;
(z `1) * (y `2) = ((z `1) * (y `2)) * (1_ I) by VECTSP_1:def_4
.= ((z `1) * (y `2)) * ((x `2) / (x `2)) by A3, GCD_1:9
.= (((z `2) * (y `1)) * (x `2)) / (x `2) by A3, A11, A8, GCD_1:11
.= ((z `2) * (y `1)) * ((x `2) / (x `2)) by A3, A9, GCD_1:11
.= ((z `2) * (y `1)) * (1_ I) by A3, GCD_1:9
.= (z `2) * (y `1) by VECTSP_1:def_4 ;
hence z in QClass. y by Def4; ::_thesis: verum
end;
( qadd (u,(q0. I)) = QClass. (padd (y,x)) & qadd ((q0. I),u) = QClass. (padd (x,y)) ) by A1, A2, Th9;
hence ( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u ) by A2, A5, A7, SUBSET_1:3; ::_thesis: verum
end;
theorem Th13: :: QUOFIELD:13
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds
( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds
( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) )
let u, v, w be Element of Quot. I; ::_thesis: ( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) )
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
consider z being Element of Q. I such that
A2: w = QClass. z by Def5;
consider y being Element of Q. I such that
A3: v = QClass. y by Def5;
A4: qmult (u,v) = QClass. (pmult (x,y)) by A1, A3, Th10
.= qmult (v,u) by A1, A3, Th10 ;
qmult (u,(qmult (v,w))) = qmult ((QClass. x),(QClass. (pmult (y,z)))) by A1, A3, A2, Th10
.= QClass. (pmult (x,(pmult (y,z)))) by Th10
.= QClass. (pmult ((pmult (x,y)),z)) by Th4
.= qmult ((QClass. (pmult (x,y))),(QClass. z)) by Th10
.= qmult ((qmult (u,v)),w) by A1, A3, A2, Th10 ;
hence ( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) ) by A4; ::_thesis: verum
end;
theorem Th14: :: QUOFIELD:14
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( qmult (u,(q1. I)) = u & qmult ((q1. I),u) = u )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I holds
( qmult (u,(q1. I)) = u & qmult ((q1. I),u) = u )
let u be Element of Quot. I; ::_thesis: ( qmult (u,(q1. I)) = u & qmult ((q1. I),u) = u )
consider x being Element of Q. I such that
A1: q1. I = QClass. x by Def5;
consider y being Element of Q. I such that
A2: u = QClass. y by Def5;
A3: x `2 <> 0. I by Th2;
y `2 <> 0. I by Th2;
then (x `2) * (y `2) <> 0. I by A3, VECTSP_2:def_1;
then reconsider t = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
XX: ( [((x `1) * (y `1)),((x `2) * (y `2))] `1 = (x `1) * (y `1) & [((x `1) * (y `1)),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
x in q1. I by A1, Th5;
then A4: x `1 = x `2 by Def9;
A5: for z being Element of Q. I st z in QClass. y holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. y implies z in QClass. t )
assume z in QClass. y ; ::_thesis: z in QClass. t
then A6: (z `1) * (y `2) = (z `2) * (y `1) by Def4;
(z `1) * (t `2) = (z `1) * ((x `2) * (y `2)) by XX
.= ((z `2) * (y `1)) * (x `2) by A6, GROUP_1:def_3
.= (z `2) * ((x `1) * (y `1)) by A4, GROUP_1:def_3
.= (z `2) * (t `1) by XX ;
hence z in QClass. t by Def4; ::_thesis: verum
end;
A7: for z being Element of Q. I st z in QClass. t holds
z in QClass. y
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies z in QClass. y )
x `2 divides x `2 ;
then A8: x `2 divides ((z `1) * (y `2)) * (x `2) by GCD_1:7;
x `2 divides x `2 ;
then A9: x `2 divides ((z `2) * (y `1)) * (x `2) by GCD_1:7;
assume z in QClass. t ; ::_thesis: z in QClass. y
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then A10: (z `1) * ((x `2) * (y `2)) = (z `2) * (t `1) by XX;
A11: ((z `1) * (y `2)) * (x `2) = (z `1) * ((x `2) * (y `2)) by GROUP_1:def_3
.= (z `2) * ((x `2) * (y `1)) by A4, A10, XX
.= ((z `2) * (y `1)) * (x `2) by GROUP_1:def_3 ;
(z `1) * (y `2) = ((z `1) * (y `2)) * (1_ I) by VECTSP_1:def_4
.= ((z `1) * (y `2)) * ((x `2) / (x `2)) by A3, GCD_1:9
.= (((z `2) * (y `1)) * (x `2)) / (x `2) by A3, A11, A8, GCD_1:11
.= ((z `2) * (y `1)) * ((x `2) / (x `2)) by A3, A9, GCD_1:11
.= ((z `2) * (y `1)) * (1_ I) by A3, GCD_1:9
.= (z `2) * (y `1) by VECTSP_1:def_4 ;
hence z in QClass. y by Def4; ::_thesis: verum
end;
( qmult (u,(q1. I)) = QClass. (pmult (y,x)) & qmult ((q1. I),u) = QClass. (pmult (x,y)) ) by A1, A2, Th10;
hence ( qmult (u,(q1. I)) = u & qmult ((q1. I),u) = u ) by A2, A5, A7, SUBSET_1:3; ::_thesis: verum
end;
theorem Th15: :: QUOFIELD:15
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w)))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w)))
let u, v, w be Element of Quot. I; ::_thesis: qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w)))
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
consider y being Element of Q. I such that
A2: v = QClass. y by Def5;
consider z being Element of Q. I such that
A3: w = QClass. z by Def5;
A4: qmult ((qadd (u,v)),w) = qmult ((QClass. (padd (x,y))),(QClass. z)) by A1, A2, A3, Th9
.= QClass. (pmult ((padd (x,y)),z)) by Th10 ;
A5: z `2 <> 0. I by Th2;
A6: y `2 <> 0. I by Th2;
then A7: (y `2) * (z `2) <> 0. I by A5, VECTSP_2:def_1;
then reconsider s2 = [((y `1) * (z `1)),((y `2) * (z `2))] as Element of Q. I by Def1;
X2: ( [((y `1) * (z `1)),((y `2) * (z `2))] `1 = (y `1) * (z `1) & [((y `1) * (z `1)),((y `2) * (z `2))] `2 = (y `2) * (z `2) ) ;
A8: x `2 <> 0. I by Th2;
then A9: (x `2) * (y `2) <> 0. I by A6, VECTSP_2:def_1;
then reconsider s = [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
X: ( [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] `1 = ((x `1) * (y `2)) + ((y `1) * (x `2)) & [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
A10: (x `2) * (z `2) <> 0. I by A8, A5, VECTSP_2:def_1;
then reconsider s1 = [((x `1) * (z `1)),((x `2) * (z `2))] as Element of Q. I by Def1;
X1: ( [((x `1) * (z `1)),((x `2) * (z `2))] `1 = (x `1) * (z `1) & [((x `1) * (z `1)),((x `2) * (z `2))] `2 = (x `2) * (z `2) ) ;
((x `2) * (z `2)) * ((y `2) * (z `2)) <> 0. I by A7, A10, VECTSP_2:def_1;
then reconsider s3 = [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] as Element of Q. I by Def1;
X3: ( [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] `1 = (((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2))) & [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] `2 = ((x `2) * (z `2)) * ((y `2) * (z `2)) ) ;
((x `2) * (y `2)) * (z `2) <> 0. I by A5, A9, VECTSP_2:def_1;
then reconsider r = [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] as Element of Q. I by Def1;
Y: ( [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] `1 = (((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1) & [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] `2 = ((x `2) * (y `2)) * (z `2) ) ;
A11: padd ((pmult (x,z)),(pmult (y,z))) = [((((x `1) * (z `1)) * (s2 `2)) + ((s2 `1) * (s1 `2))),((s1 `2) * (s2 `2))] by X1
.= [((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((s2 `1) * (s1 `2))),((s1 `2) * (s2 `2))] by X2
.= [((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((s2 `1) * (s1 `2))),((s1 `2) * ((y `2) * (z `2)))] by X2
.= [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * (s1 `2))),((s1 `2) * ((y `2) * (z `2)))] by X2
.= [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),((s1 `2) * ((y `2) * (z `2)))] by X1
.= [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] by X1 ;
A12: pmult ((padd (x,y)),z) = [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),((s `2) * (z `2))] by X
.= [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] by X ;
A13: for t being Element of Q. I st t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) holds
t in QClass. (pmult ((padd (x,y)),z))
proof
let t be Element of Q. I; ::_thesis: ( t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) implies t in QClass. (pmult ((padd (x,y)),z)) )
assume t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) ; ::_thesis: t in QClass. (pmult ((padd (x,y)),z))
then (t `1) * (s3 `2) = (t `2) * (s3 `1) by A11, Def4;
then (t `1) * (((x `2) * (z `2)) * ((y `2) * (z `2))) = (t `2) * (s3 `1) by X3;
then A14: (t `1) * (((x `2) * (z `2)) * ((y `2) * (z `2))) = (t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))) by X3;
((t `1) * (((x `2) * (y `2)) * (z `2))) * (z `2) = (t `1) * ((((x `2) * (y `2)) * (z `2)) * (z `2)) by GROUP_1:def_3
.= (t `1) * (((x `2) * ((y `2) * (z `2))) * (z `2)) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))) by A14, GROUP_1:def_3
.= (t `2) * (((((x `1) * (z `1)) * (y `2)) * (z `2)) + (((y `1) * (z `1)) * ((x `2) * (z `2)))) by GROUP_1:def_3
.= (t `2) * (((((x `1) * (z `1)) * (y `2)) * (z `2)) + ((((y `1) * (z `1)) * (x `2)) * (z `2))) by GROUP_1:def_3
.= (t `2) * (((((x `1) * (z `1)) * (y `2)) + (((y `1) * (z `1)) * (x `2))) * (z `2)) by VECTSP_1:def_3
.= (t `2) * ((((z `1) * ((x `1) * (y `2))) + (((y `1) * (z `1)) * (x `2))) * (z `2)) by GROUP_1:def_3
.= (t `2) * ((((z `1) * ((x `1) * (y `2))) + ((z `1) * ((y `1) * (x `2)))) * (z `2)) by GROUP_1:def_3
.= (t `2) * (((z `1) * (((x `1) * (y `2)) + ((y `1) * (x `2)))) * (z `2)) by VECTSP_1:def_2
.= ((t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1))) * (z `2) by GROUP_1:def_3 ;
then (t `1) * (((x `2) * (y `2)) * (z `2)) = (t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) by A5, GCD_1:1;
then (t `1) * (r `2) = (t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) by Y
.= (t `2) * (r `1) by Y ;
hence t in QClass. (pmult ((padd (x,y)),z)) by A12, Def4; ::_thesis: verum
end;
A15: for t being Element of Q. I st t in QClass. (pmult ((padd (x,y)),z)) holds
t in QClass. (padd ((pmult (x,z)),(pmult (y,z))))
proof
let t be Element of Q. I; ::_thesis: ( t in QClass. (pmult ((padd (x,y)),z)) implies t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) )
assume t in QClass. (pmult ((padd (x,y)),z)) ; ::_thesis: t in QClass. (padd ((pmult (x,z)),(pmult (y,z))))
then (t `1) * (r `2) = (t `2) * (r `1) by A12, Def4;
then (t `1) * (((x `2) * (y `2)) * (z `2)) = (t `2) * (r `1) by Y;
then A16: (t `1) * (((x `2) * (y `2)) * (z `2)) = (t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) by Y;
(t `1) * (s3 `2) = (t `1) * (((x `2) * (z `2)) * ((y `2) * (z `2))) by X3
.= (t `1) * ((((x `2) * (z `2)) * (y `2)) * (z `2)) by GROUP_1:def_3
.= ((t `1) * (((x `2) * (z `2)) * (y `2))) * (z `2) by GROUP_1:def_3
.= ((t `1) * (((x `2) * (y `2)) * (z `2))) * (z `2) by GROUP_1:def_3
.= (t `2) * (((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) * (z `2)) by A16, GROUP_1:def_3
.= (t `2) * (((((x `1) * (y `2)) * (z `1)) + (((y `1) * (x `2)) * (z `1))) * (z `2)) by VECTSP_1:def_3
.= (t `2) * (((((x `1) * (y `2)) * (z `1)) * (z `2)) + ((((y `1) * (x `2)) * (z `1)) * (z `2))) by VECTSP_1:def_3
.= (t `2) * ((((y `2) * ((x `1) * (z `1))) * (z `2)) + ((((y `1) * (x `2)) * (z `1)) * (z `2))) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((((y `1) * (x `2)) * (z `1)) * (z `2))) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((((y `1) * (z `1)) * (x `2)) * (z `2))) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))) by GROUP_1:def_3
.= (t `2) * (s3 `1) by X3 ;
hence t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) by A11, Def4; ::_thesis: verum
end;
qadd ((qmult (u,w)),(qmult (v,w))) = qadd ((QClass. (pmult (x,z))),(qmult ((QClass. y),(QClass. z)))) by A1, A2, A3, Th10
.= qadd ((QClass. (pmult (x,z))),(QClass. (pmult (y,z)))) by Th10
.= QClass. (padd ((pmult (x,z)),(pmult (y,z)))) by Th9 ;
hence qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w))) by A4, A15, A13, SUBSET_1:3; ::_thesis: verum
end;
theorem Th16: :: QUOFIELD:16
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w)))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w)))
let u, v, w be Element of Quot. I; ::_thesis: qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w)))
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
consider y being Element of Q. I such that
A2: v = QClass. y by Def5;
consider z being Element of Q. I such that
A3: w = QClass. z by Def5;
A4: x `2 <> 0. I by Th2;
A5: z `2 <> 0. I by Th2;
then A6: (x `2) * (z `2) <> 0. I by A4, VECTSP_2:def_1;
then reconsider s2 = [((x `1) * (z `1)),((x `2) * (z `2))] as Element of Q. I by Def1;
X2: ( [((x `1) * (z `1)),((x `2) * (z `2))] `1 = (x `1) * (z `1) & [((x `1) * (z `1)),((x `2) * (z `2))] `2 = (x `2) * (z `2) ) ;
A7: y `2 <> 0. I by Th2;
then A8: (y `2) * (z `2) <> 0. I by A5, VECTSP_2:def_1;
then reconsider s = [(((y `1) * (z `2)) + ((z `1) * (y `2))),((y `2) * (z `2))] as Element of Q. I by Def1;
X: ( [(((y `1) * (z `2)) + ((z `1) * (y `2))),((y `2) * (z `2))] `1 = ((y `1) * (z `2)) + ((z `1) * (y `2)) & [(((y `1) * (z `2)) + ((z `1) * (y `2))),((y `2) * (z `2))] `2 = (y `2) * (z `2) ) ;
A9: (x `2) * (y `2) <> 0. I by A4, A7, VECTSP_2:def_1;
then reconsider s1 = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
X1: ( [((x `1) * (y `1)),((x `2) * (y `2))] `1 = (x `1) * (y `1) & [((x `1) * (y `1)),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
((x `2) * (y `2)) * ((x `2) * (z `2)) <> 0. I by A9, A6, VECTSP_2:def_1;
then reconsider s3 = [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * ((x `2) * (z `2)))] as Element of Q. I by Def1;
X3: ( [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * ((x `2) * (z `2)))] `1 = (((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2))) & [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * ((x `2) * (z `2)))] `2 = ((x `2) * (y `2)) * ((x `2) * (z `2)) ) ;
(x `2) * ((y `2) * (z `2)) <> 0. I by A4, A8, VECTSP_2:def_1;
then reconsider r = [((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))),((x `2) * ((y `2) * (z `2)))] as Element of Q. I by Def1;
Y: ( [((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))),((x `2) * ((y `2) * (z `2)))] `1 = (x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))) & [((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))),((x `2) * ((y `2) * (z `2)))] `2 = (x `2) * ((y `2) * (z `2)) ) ;
A10: padd ((pmult (x,y)),(pmult (x,z))) = [((((x `1) * (y `1)) * (s2 `2)) + ((s2 `1) * (s1 `2))),((s1 `2) * (s2 `2))] by X1
.= [((((x `1) * (y `1)) * ((x `2) * (z `2))) + ((s2 `1) * (s1 `2))),((s1 `2) * (s2 `2))] by X2
.= [((((x `1) * (y `1)) * ((x `2) * (z `2))) + ((s2 `1) * (s1 `2))),((s1 `2) * ((x `2) * (z `2)))] by X2
.= [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * (s1 `2))),((s1 `2) * ((x `2) * (z `2)))] by X2
.= [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))),((s1 `2) * ((x `2) * (z `2)))] by X1
.= [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * ((x `2) * (z `2)))] by X1 ;
A11: pmult (x,(padd (y,z))) = [((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))),((x `2) * (s `2))] by X
.= [((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))),((x `2) * ((y `2) * (z `2)))] by X ;
A12: for t being Element of Q. I st t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) holds
t in QClass. (pmult (x,(padd (y,z))))
proof
let t be Element of Q. I; ::_thesis: ( t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) implies t in QClass. (pmult (x,(padd (y,z)))) )
assume t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) ; ::_thesis: t in QClass. (pmult (x,(padd (y,z))))
then (t `1) * (s3 `2) = (t `2) * (s3 `1) by A10, Def4;
then (t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2))) = (t `2) * (s3 `1) by X3;
then A13: (t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2))) = (t `2) * ((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))) by X3;
((t `1) * ((x `2) * ((y `2) * (z `2)))) * (x `2) = ((t `1) * (((x `2) * (y `2)) * (z `2))) * (x `2) by GROUP_1:def_3
.= (t `1) * ((((x `2) * (y `2)) * (z `2)) * (x `2)) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))) by A13, GROUP_1:def_3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) * (x `2)) + (((x `1) * (z `1)) * ((x `2) * (y `2)))) by GROUP_1:def_3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) * (x `2)) + ((((x `1) * (z `1)) * (y `2)) * (x `2))) by GROUP_1:def_3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) + (((x `1) * (z `1)) * (y `2))) * (x `2)) by VECTSP_1:def_3
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) + (((x `1) * (z `1)) * (y `2))) * (x `2)) by GROUP_1:def_3
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) + ((x `1) * ((z `1) * (y `2)))) * (x `2)) by GROUP_1:def_3
.= (t `2) * (((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) * (x `2)) by VECTSP_1:def_2
.= ((t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))))) * (x `2) by GROUP_1:def_3 ;
then (t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) by A4, GCD_1:1;
then (t `1) * (r `2) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) by Y
.= (t `2) * (r `1) by Y ;
hence t in QClass. (pmult (x,(padd (y,z)))) by A11, Def4; ::_thesis: verum
end;
A14: for t being Element of Q. I st t in QClass. (pmult (x,(padd (y,z)))) holds
t in QClass. (padd ((pmult (x,y)),(pmult (x,z))))
proof
let t be Element of Q. I; ::_thesis: ( t in QClass. (pmult (x,(padd (y,z)))) implies t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) )
assume t in QClass. (pmult (x,(padd (y,z)))) ; ::_thesis: t in QClass. (padd ((pmult (x,y)),(pmult (x,z))))
then (t `1) * (r `2) = (t `2) * (r `1) by A11, Def4;
then (t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * (r `1) by Y;
then A15: (t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) by Y;
(t `1) * (s3 `2) = (t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2))) by X3
.= (t `1) * ((((x `2) * (y `2)) * (z `2)) * (x `2)) by GROUP_1:def_3
.= ((t `1) * (((x `2) * (y `2)) * (z `2))) * (x `2) by GROUP_1:def_3
.= ((t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))))) * (x `2) by A15, GROUP_1:def_3
.= (t `2) * (((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) * (x `2)) by GROUP_1:def_3
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) + ((x `1) * ((z `1) * (y `2)))) * (x `2)) by VECTSP_1:def_2
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) * (x `2)) + (((x `1) * ((z `1) * (y `2))) * (x `2))) by VECTSP_1:def_3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) * (x `2)) + (((x `1) * ((z `1) * (y `2))) * (x `2))) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (y `1)) * ((z `2) * (x `2))) + (((x `1) * ((z `1) * (y `2))) * (x `2))) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (y `1)) * ((z `2) * (x `2))) + ((((x `1) * (z `1)) * (y `2)) * (x `2))) by GROUP_1:def_3
.= (t `2) * ((((x `1) * (y `1)) * ((z `2) * (x `2))) + (((x `1) * (z `1)) * ((y `2) * (x `2)))) by GROUP_1:def_3
.= (t `2) * (s3 `1) by X3 ;
hence t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) by A10, Def4; ::_thesis: verum
end;
A16: qmult (u,(qadd (v,w))) = qmult ((QClass. x),(QClass. (padd (y,z)))) by A1, A2, A3, Th9
.= QClass. (pmult (x,(padd (y,z)))) by Th10 ;
qadd ((qmult (u,v)),(qmult (u,w))) = qadd ((QClass. (pmult (x,y))),(qmult ((QClass. x),(QClass. z)))) by A1, A2, A3, Th10
.= qadd ((QClass. (pmult (x,y))),(QClass. (pmult (x,z)))) by Th10
.= QClass. (padd ((pmult (x,y)),(pmult (x,z)))) by Th9 ;
hence qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w))) by A16, A14, A12, SUBSET_1:3; ::_thesis: verum
end;
theorem Th17: :: QUOFIELD:17
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I holds
( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I )
let u be Element of Quot. I; ::_thesis: ( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I )
consider x being Element of Q. I such that
A1: qaddinv u = QClass. x by Def5;
x in qaddinv u by A1, Th5;
then consider a being Element of Q. I such that
A2: a in u and
A3: (x `1) * (a `2) = (x `2) * (- (a `1)) by Def10;
consider y being Element of Q. I such that
A4: u = QClass. y by Def5;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then (x `2) * (y `2) <> 0. I by VECTSP_2:def_1;
then reconsider t = [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
XX: ( [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] `1 = ((y `1) * (x `2)) + ((x `1) * (y `2)) & [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
A5: a `2 <> 0. I by Th2;
y in u by A4, Th5;
then A6: (y `1) * (a `2) = (a `1) * (y `2) by A2, Th7;
(t `1) * (a `2) = (((y `1) * (x `2)) + ((x `1) * (y `2))) * (a `2) by XX
.= (((y `1) * (x `2)) * (a `2)) + (((x `1) * (y `2)) * (a `2)) by VECTSP_1:def_3
.= ((x `2) * ((a `1) * (y `2))) + (((x `1) * (y `2)) * (a `2)) by A6, GROUP_1:def_3
.= ((x `2) * ((a `1) * (y `2))) + (((x `2) * (- (a `1))) * (y `2)) by A3, GROUP_1:def_3
.= ((x `2) * ((a `1) * (y `2))) + ((- ((x `2) * (a `1))) * (y `2)) by GCD_1:48
.= ((x `2) * ((a `1) * (y `2))) + (- (((x `2) * (a `1)) * (y `2))) by GCD_1:48
.= (((x `2) * (a `1)) * (y `2)) + (- (((x `2) * (a `1)) * (y `2))) by GROUP_1:def_3
.= 0. I by RLVECT_1:def_10 ;
then A7: t `1 = 0. I by A5, VECTSP_2:def_1;
A8: for z being Element of Q. I st z in q0. I holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( z in q0. I implies z in QClass. t )
assume z in q0. I ; ::_thesis: z in QClass. t
then z `1 = 0. I by Def8;
then A9: (z `1) * (t `2) = 0. I by VECTSP_1:7;
(z `2) * (t `1) = 0. I by A7, VECTSP_1:7;
hence z in QClass. t by A9, Def4; ::_thesis: verum
end;
A10: t `2 <> 0. I by Th2;
A11: for z being Element of Q. I st z in QClass. t holds
z in q0. I
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies z in q0. I )
assume z in QClass. t ; ::_thesis: z in q0. I
then A12: (z `1) * (t `2) = (z `2) * (t `1) by Def4;
(z `2) * (t `1) = 0. I by A7, VECTSP_1:7;
then z `1 = 0. I by A10, A12, VECTSP_2:def_1;
hence z in q0. I by Def8; ::_thesis: verum
end;
( qadd (u,(qaddinv u)) = QClass. (padd (y,x)) & qadd ((qaddinv u),u) = QClass. (padd (x,y)) ) by A1, A4, Th9;
hence ( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I ) by A11, A8, SUBSET_1:3; ::_thesis: verum
end;
theorem Th18: :: QUOFIELD:18
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I st u <> q0. I holds
( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I st u <> q0. I holds
( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )
let u be Element of Quot. I; ::_thesis: ( u <> q0. I implies ( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I ) )
assume A1: u <> q0. I ; ::_thesis: ( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )
consider x being Element of Q. I such that
A2: qmultinv u = QClass. x by Def5;
consider y being Element of Q. I such that
A3: u = QClass. y by Def5;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then A4: (x `2) * (y `2) <> 0. I by VECTSP_2:def_1;
then reconsider t = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
XX: ( [((x `1) * (y `1)),((x `2) * (y `2))] `1 = (x `1) * (y `1) & [((x `1) * (y `1)),((x `2) * (y `2))] `2 = (x `2) * (y `2) ) ;
x in qmultinv u by A2, Th5;
then consider a being Element of Q. I such that
A5: a in u and
A6: (x `1) * (a `1) = (x `2) * (a `2) by A1, Def11;
y in u by A3, Th5;
then A7: (y `1) * (a `2) = (a `1) * (y `2) by A5, Th7;
A8: a `1 <> 0. I
proof
assume a `1 = 0. I ; ::_thesis: contradiction
then a in q0. I by Def8;
then a in (q0. I) /\ u by A5, XBOOLE_0:def_4;
then q0. I meets u by XBOOLE_0:4;
hence contradiction by A1, Th8; ::_thesis: verum
end;
A9: a `2 <> 0. I by Th2;
A10: for z being Element of Q. I st z in q1. I holds
z in QClass. t
proof
let z be Element of Q. I; ::_thesis: ( z in q1. I implies z in QClass. t )
assume z in q1. I ; ::_thesis: z in QClass. t
then z `1 = z `2 by Def9;
then A11: ((z `1) * (t `2)) * ((a `1) * (a `2)) = ((z `2) * ((x `2) * (y `2))) * ((a `1) * (a `2)) by XX
.= (z `2) * (((x `2) * (y `2)) * ((a `1) * (a `2))) by GROUP_1:def_3
.= (z `2) * ((x `2) * ((y `2) * ((a `1) * (a `2)))) by GROUP_1:def_3
.= (z `2) * ((x `2) * (((y `1) * (a `2)) * (a `2))) by A7, GROUP_1:def_3
.= (z `2) * (((x `1) * (a `1)) * ((y `1) * (a `2))) by A6, GROUP_1:def_3
.= (z `2) * ((x `1) * ((a `1) * ((y `1) * (a `2)))) by GROUP_1:def_3
.= (z `2) * ((x `1) * ((y `1) * ((a `1) * (a `2)))) by GROUP_1:def_3
.= (z `2) * (((x `1) * (y `1)) * ((a `1) * (a `2))) by GROUP_1:def_3
.= ((z `2) * ((x `1) * (y `1))) * ((a `1) * (a `2)) by GROUP_1:def_3
.= ((z `2) * (t `1)) * ((a `1) * (a `2)) by XX ;
(a `1) * (a `2) <> 0. I by A8, A9, VECTSP_2:def_1;
then (z `1) * (t `2) = (z `2) * (t `1) by A11, GCD_1:1;
hence z in QClass. t by Def4; ::_thesis: verum
end;
A12: for z being Element of Q. I st z in QClass. t holds
z in q1. I
proof
let z be Element of Q. I; ::_thesis: ( z in QClass. t implies z in q1. I )
assume z in QClass. t ; ::_thesis: z in q1. I
then A13: (z `1) * (t `2) = (z `2) * (t `1) by Def4;
(a `2) * (a `1) <> 0. I by A8, A9, VECTSP_2:def_1;
then A14: ((x `2) * (y `2)) * ((a `2) * (a `1)) <> 0. I by A4, VECTSP_2:def_1;
(z `1) * (((x `2) * (y `2)) * ((a `1) * (a `2))) = ((z `1) * ((x `2) * (y `2))) * ((a `1) * (a `2)) by GROUP_1:def_3
.= ((z `2) * (t `1)) * ((a `1) * (a `2)) by A13, XX
.= ((z `2) * ((x `1) * (y `1))) * ((a `1) * (a `2)) by XX
.= (z `2) * (((x `1) * (y `1)) * ((a `1) * (a `2))) by GROUP_1:def_3
.= (z `2) * ((((y `1) * (x `1)) * (a `1)) * (a `2)) by GROUP_1:def_3
.= (z `2) * (((y `1) * ((x `2) * (a `2))) * (a `2)) by A6, GROUP_1:def_3
.= (z `2) * (((x `2) * (a `2)) * ((a `1) * (y `2))) by A7, GROUP_1:def_3
.= (z `2) * ((x `2) * ((a `2) * ((a `1) * (y `2)))) by GROUP_1:def_3
.= (z `2) * ((x `2) * ((y `2) * ((a `2) * (a `1)))) by GROUP_1:def_3
.= (z `2) * (((x `2) * (y `2)) * ((a `2) * (a `1))) by GROUP_1:def_3 ;
then z `1 = z `2 by A14, GCD_1:1;
hence z in q1. I by Def9; ::_thesis: verum
end;
( qmult (u,(qmultinv u)) = QClass. (pmult (y,x)) & qmult ((qmultinv u),u) = QClass. (pmult (x,y)) ) by A2, A3, Th10;
hence ( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I ) by A12, A10, SUBSET_1:3; ::_thesis: verum
end;
theorem Th19: :: QUOFIELD:19
for I being non degenerated commutative domRing-like Ring holds q1. I <> q0. I
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: q1. I <> q0. I
reconsider t = [(0. I),(1_ I)] as Element of Q. I by Def1;
XX: ( [(0. I),(1_ I)] `1 = 0. I & [(0. I),(1_ I)] `2 = 1_ I ) ;
assume A1: q1. I = q0. I ; ::_thesis: contradiction
t `1 = 0. I by XX;
then t in q0. I by Def8;
then t `1 = t `2 by A1, Def9;
hence contradiction by XX; ::_thesis: verum
end;
definition
let I be non degenerated commutative domRing-like Ring;
func quotadd I -> BinOp of (Quot. I) means :Def12: :: QUOFIELD:def 12
for u, v being Element of Quot. I holds it . (u,v) = qadd (u,v);
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v)
proof
deffunc H1( Element of Quot. I, Element of Quot. I) -> Element of Quot. I = qadd ($1,$2);
consider F being BinOp of (Quot. I) such that
A1: for u, v being Element of Quot. I holds F . (u,v) = H1(u,v) from BINOP_1:sch_4();
take F ; ::_thesis: for u, v being Element of Quot. I holds F . (u,v) = qadd (u,v)
let u, v be Element of Quot. I; ::_thesis: F . (u,v) = qadd (u,v)
thus F . (u,v) = qadd (u,v) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qadd (u,v) ) holds
b1 = b2
proof
let F1, F2 be BinOp of (Quot. I); ::_thesis: ( ( for u, v being Element of Quot. I holds F1 . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds F2 . (u,v) = qadd (u,v) ) implies F1 = F2 )
assume that
A2: for u, v being Element of Quot. I holds F1 . (u,v) = qadd (u,v) and
A3: for u, v being Element of Quot. I holds F2 . (u,v) = qadd (u,v) ; ::_thesis: F1 = F2
now__::_thesis:_for_u,_v_being_Element_of_Quot._I_holds_F1_._(u,v)_=_F2_._(u,v)
let u, v be Element of Quot. I; ::_thesis: F1 . (u,v) = F2 . (u,v)
thus F1 . (u,v) = qadd (u,v) by A2
.= F2 . (u,v) by A3 ; ::_thesis: verum
end;
hence F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines quotadd QUOFIELD:def_12_:_
for I being non degenerated commutative domRing-like Ring
for b2 being BinOp of (Quot. I) holds
( b2 = quotadd I iff for u, v being Element of Quot. I holds b2 . (u,v) = qadd (u,v) );
definition
let I be non degenerated commutative domRing-like Ring;
func quotmult I -> BinOp of (Quot. I) means :Def13: :: QUOFIELD:def 13
for u, v being Element of Quot. I holds it . (u,v) = qmult (u,v);
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qmult (u,v)
proof
deffunc H1( Element of Quot. I, Element of Quot. I) -> Element of Quot. I = qmult ($1,$2);
consider F being BinOp of (Quot. I) such that
A1: for u, v being Element of Quot. I holds F . (u,v) = H1(u,v) from BINOP_1:sch_4();
take F ; ::_thesis: for u, v being Element of Quot. I holds F . (u,v) = qmult (u,v)
let u, v be Element of Quot. I; ::_thesis: F . (u,v) = qmult (u,v)
thus F . (u,v) = qmult (u,v) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qmult (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qmult (u,v) ) holds
b1 = b2
proof
let F1, F2 be BinOp of (Quot. I); ::_thesis: ( ( for u, v being Element of Quot. I holds F1 . (u,v) = qmult (u,v) ) & ( for u, v being Element of Quot. I holds F2 . (u,v) = qmult (u,v) ) implies F1 = F2 )
assume that
A2: for u, v being Element of Quot. I holds F1 . (u,v) = qmult (u,v) and
A3: for u, v being Element of Quot. I holds F2 . (u,v) = qmult (u,v) ; ::_thesis: F1 = F2
now__::_thesis:_for_u,_v_being_Element_of_Quot._I_holds_F1_._(u,v)_=_F2_._(u,v)
let u, v be Element of Quot. I; ::_thesis: F1 . (u,v) = F2 . (u,v)
thus F1 . (u,v) = qmult (u,v) by A2
.= F2 . (u,v) by A3 ; ::_thesis: verum
end;
hence F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines quotmult QUOFIELD:def_13_:_
for I being non degenerated commutative domRing-like Ring
for b2 being BinOp of (Quot. I) holds
( b2 = quotmult I iff for u, v being Element of Quot. I holds b2 . (u,v) = qmult (u,v) );
definition
let I be non degenerated commutative domRing-like Ring;
func quotaddinv I -> UnOp of (Quot. I) means :Def14: :: QUOFIELD:def 14
for u being Element of Quot. I holds it . u = qaddinv u;
existence
ex b1 being UnOp of (Quot. I) st
for u being Element of Quot. I holds b1 . u = qaddinv u
proof
deffunc H1( Element of Quot. I) -> Element of Quot. I = qaddinv $1;
consider F being UnOp of (Quot. I) such that
A1: for u being Element of Quot. I holds F . u = H1(u) from FUNCT_2:sch_4();
take F ; ::_thesis: for u being Element of Quot. I holds F . u = qaddinv u
let u be Element of Quot. I; ::_thesis: F . u = qaddinv u
thus F . u = qaddinv u by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b1 . u = qaddinv u ) & ( for u being Element of Quot. I holds b2 . u = qaddinv u ) holds
b1 = b2
proof
let F1, F2 be UnOp of (Quot. I); ::_thesis: ( ( for u being Element of Quot. I holds F1 . u = qaddinv u ) & ( for u being Element of Quot. I holds F2 . u = qaddinv u ) implies F1 = F2 )
assume that
A2: for u being Element of Quot. I holds F1 . u = qaddinv u and
A3: for u being Element of Quot. I holds F2 . u = qaddinv u ; ::_thesis: F1 = F2
now__::_thesis:_for_u_being_Element_of_Quot._I_holds_F1_=_F2
let u be Element of Quot. I; ::_thesis: F1 = F2
A4: for u being set st u in Quot. I holds
F1 . u = F2 . u
proof
let u be set ; ::_thesis: ( u in Quot. I implies F1 . u = F2 . u )
assume u in Quot. I ; ::_thesis: F1 . u = F2 . u
then reconsider u = u as Element of Quot. I ;
F1 . u = qaddinv u by A2
.= F2 . u by A3 ;
hence F1 . u = F2 . u ; ::_thesis: verum
end;
( Quot. I = dom F1 & Quot. I = dom F2 ) by FUNCT_2:def_1;
hence F1 = F2 by A4, FUNCT_1:2; ::_thesis: verum
end;
hence F1 = F2 ; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines quotaddinv QUOFIELD:def_14_:_
for I being non degenerated commutative domRing-like Ring
for b2 being UnOp of (Quot. I) holds
( b2 = quotaddinv I iff for u being Element of Quot. I holds b2 . u = qaddinv u );
definition
let I be non degenerated commutative domRing-like Ring;
func quotmultinv I -> UnOp of (Quot. I) means :Def15: :: QUOFIELD:def 15
for u being Element of Quot. I holds it . u = qmultinv u;
existence
ex b1 being UnOp of (Quot. I) st
for u being Element of Quot. I holds b1 . u = qmultinv u
proof
deffunc H1( Element of Quot. I) -> Element of Quot. I = qmultinv $1;
consider F being UnOp of (Quot. I) such that
A1: for u being Element of Quot. I holds F . u = H1(u) from FUNCT_2:sch_4();
take F ; ::_thesis: for u being Element of Quot. I holds F . u = qmultinv u
let u be Element of Quot. I; ::_thesis: F . u = qmultinv u
thus F . u = qmultinv u by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b1 . u = qmultinv u ) & ( for u being Element of Quot. I holds b2 . u = qmultinv u ) holds
b1 = b2
proof
let F1, F2 be UnOp of (Quot. I); ::_thesis: ( ( for u being Element of Quot. I holds F1 . u = qmultinv u ) & ( for u being Element of Quot. I holds F2 . u = qmultinv u ) implies F1 = F2 )
assume that
A2: for u being Element of Quot. I holds F1 . u = qmultinv u and
A3: for u being Element of Quot. I holds F2 . u = qmultinv u ; ::_thesis: F1 = F2
now__::_thesis:_for_u_being_Element_of_Quot._I_holds_F1_=_F2
let u be Element of Quot. I; ::_thesis: F1 = F2
A4: for u being set st u in Quot. I holds
F1 . u = F2 . u
proof
let u be set ; ::_thesis: ( u in Quot. I implies F1 . u = F2 . u )
assume u in Quot. I ; ::_thesis: F1 . u = F2 . u
then reconsider u = u as Element of Quot. I ;
F1 . u = qmultinv u by A2
.= F2 . u by A3 ;
hence F1 . u = F2 . u ; ::_thesis: verum
end;
( Quot. I = dom F1 & Quot. I = dom F2 ) by FUNCT_2:def_1;
hence F1 = F2 by A4, FUNCT_1:2; ::_thesis: verum
end;
hence F1 = F2 ; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines quotmultinv QUOFIELD:def_15_:_
for I being non degenerated commutative domRing-like Ring
for b2 being UnOp of (Quot. I) holds
( b2 = quotmultinv I iff for u being Element of Quot. I holds b2 . u = qmultinv u );
theorem Th20: :: QUOFIELD:20
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds (quotadd I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (u,((quotadd I) . (v,w)))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds (quotadd I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (u,((quotadd I) . (v,w)))
let u, v, w be Element of Quot. I; ::_thesis: (quotadd I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (u,((quotadd I) . (v,w)))
(quotadd I) . (((quotadd I) . (u,v)),w) = (quotadd I) . ((qadd (u,v)),w) by Def12
.= qadd ((qadd (u,v)),w) by Def12
.= qadd (u,(qadd (v,w))) by Th11
.= qadd (u,((quotadd I) . (v,w))) by Def12
.= (quotadd I) . (u,((quotadd I) . (v,w))) by Def12 ;
hence (quotadd I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (u,((quotadd I) . (v,w))) ; ::_thesis: verum
end;
theorem Th21: :: QUOFIELD:21
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Quot. I holds (quotadd I) . (u,v) = (quotadd I) . (v,u)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of Quot. I holds (quotadd I) . (u,v) = (quotadd I) . (v,u)
let u, v be Element of Quot. I; ::_thesis: (quotadd I) . (u,v) = (quotadd I) . (v,u)
(quotadd I) . (u,v) = qadd (u,v) by Def12
.= qadd (v,u) by Th11
.= (quotadd I) . (v,u) by Def12 ;
hence (quotadd I) . (u,v) = (quotadd I) . (v,u) ; ::_thesis: verum
end;
theorem Th22: :: QUOFIELD:22
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( (quotadd I) . (u,(q0. I)) = u & (quotadd I) . ((q0. I),u) = u )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I holds
( (quotadd I) . (u,(q0. I)) = u & (quotadd I) . ((q0. I),u) = u )
let u be Element of Quot. I; ::_thesis: ( (quotadd I) . (u,(q0. I)) = u & (quotadd I) . ((q0. I),u) = u )
A1: (quotadd I) . ((q0. I),u) = qadd ((q0. I),u) by Def12
.= u by Th12 ;
(quotadd I) . (u,(q0. I)) = qadd (u,(q0. I)) by Def12
.= u by Th12 ;
hence ( (quotadd I) . (u,(q0. I)) = u & (quotadd I) . ((q0. I),u) = u ) by A1; ::_thesis: verum
end;
theorem Th23: :: QUOFIELD:23
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds (quotmult I) . (((quotmult I) . (u,v)),w) = (quotmult I) . (u,((quotmult I) . (v,w)))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds (quotmult I) . (((quotmult I) . (u,v)),w) = (quotmult I) . (u,((quotmult I) . (v,w)))
let u, v, w be Element of Quot. I; ::_thesis: (quotmult I) . (((quotmult I) . (u,v)),w) = (quotmult I) . (u,((quotmult I) . (v,w)))
(quotmult I) . (((quotmult I) . (u,v)),w) = (quotmult I) . ((qmult (u,v)),w) by Def13
.= qmult ((qmult (u,v)),w) by Def13
.= qmult (u,(qmult (v,w))) by Th13
.= qmult (u,((quotmult I) . (v,w))) by Def13
.= (quotmult I) . (u,((quotmult I) . (v,w))) by Def13 ;
hence (quotmult I) . (((quotmult I) . (u,v)),w) = (quotmult I) . (u,((quotmult I) . (v,w))) ; ::_thesis: verum
end;
theorem Th24: :: QUOFIELD:24
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Quot. I holds (quotmult I) . (u,v) = (quotmult I) . (v,u)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of Quot. I holds (quotmult I) . (u,v) = (quotmult I) . (v,u)
let u, v be Element of Quot. I; ::_thesis: (quotmult I) . (u,v) = (quotmult I) . (v,u)
(quotmult I) . (u,v) = qmult (u,v) by Def13
.= qmult (v,u) by Th13
.= (quotmult I) . (v,u) by Def13 ;
hence (quotmult I) . (u,v) = (quotmult I) . (v,u) ; ::_thesis: verum
end;
theorem Th25: :: QUOFIELD:25
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I holds
( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )
let u be Element of Quot. I; ::_thesis: ( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )
A1: (quotmult I) . ((q1. I),u) = qmult ((q1. I),u) by Def13
.= u by Th14 ;
(quotmult I) . (u,(q1. I)) = qmult (u,(q1. I)) by Def13
.= u by Th14 ;
hence ( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u ) by A1; ::_thesis: verum
end;
theorem Th26: :: QUOFIELD:26
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds (quotmult I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (((quotmult I) . (u,w)),((quotmult I) . (v,w)))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds (quotmult I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (((quotmult I) . (u,w)),((quotmult I) . (v,w)))
let u, v, w be Element of Quot. I; ::_thesis: (quotmult I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (((quotmult I) . (u,w)),((quotmult I) . (v,w)))
(quotmult I) . (((quotadd I) . (u,v)),w) = (quotmult I) . ((qadd (u,v)),w) by Def12
.= qmult ((qadd (u,v)),w) by Def13
.= qadd ((qmult (u,w)),(qmult (v,w))) by Th15
.= qadd (((quotmult I) . (u,w)),(qmult (v,w))) by Def13
.= qadd (((quotmult I) . (u,w)),((quotmult I) . (v,w))) by Def13
.= (quotadd I) . (((quotmult I) . (u,w)),((quotmult I) . (v,w))) by Def12 ;
hence (quotmult I) . (((quotadd I) . (u,v)),w) = (quotadd I) . (((quotmult I) . (u,w)),((quotmult I) . (v,w))) ; ::_thesis: verum
end;
theorem Th27: :: QUOFIELD:27
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w)))
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v, w being Element of Quot. I holds (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w)))
let u, v, w be Element of Quot. I; ::_thesis: (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w)))
(quotmult I) . (u,((quotadd I) . (v,w))) = (quotmult I) . (u,(qadd (v,w))) by Def12
.= qmult (u,(qadd (v,w))) by Def13
.= qadd ((qmult (u,v)),(qmult (u,w))) by Th16
.= qadd (((quotmult I) . (u,v)),(qmult (u,w))) by Def13
.= qadd (((quotmult I) . (u,v)),((quotmult I) . (u,w))) by Def13
.= (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w))) by Def12 ;
hence (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w))) ; ::_thesis: verum
end;
theorem Th28: :: QUOFIELD:28
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( (quotadd I) . (u,((quotaddinv I) . u)) = q0. I & (quotadd I) . (((quotaddinv I) . u),u) = q0. I )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I holds
( (quotadd I) . (u,((quotaddinv I) . u)) = q0. I & (quotadd I) . (((quotaddinv I) . u),u) = q0. I )
let u be Element of Quot. I; ::_thesis: ( (quotadd I) . (u,((quotaddinv I) . u)) = q0. I & (quotadd I) . (((quotaddinv I) . u),u) = q0. I )
A1: (quotadd I) . (((quotaddinv I) . u),u) = (quotadd I) . ((qaddinv u),u) by Def14
.= qadd ((qaddinv u),u) by Def12
.= q0. I by Th17 ;
(quotadd I) . (u,((quotaddinv I) . u)) = (quotadd I) . (u,(qaddinv u)) by Def14
.= qadd (u,(qaddinv u)) by Def12
.= q0. I by Th17 ;
hence ( (quotadd I) . (u,((quotaddinv I) . u)) = q0. I & (quotadd I) . (((quotaddinv I) . u),u) = q0. I ) by A1; ::_thesis: verum
end;
theorem Th29: :: QUOFIELD:29
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I st u <> q0. I holds
( (quotmult I) . (u,((quotmultinv I) . u)) = q1. I & (quotmult I) . (((quotmultinv I) . u),u) = q1. I )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of Quot. I st u <> q0. I holds
( (quotmult I) . (u,((quotmultinv I) . u)) = q1. I & (quotmult I) . (((quotmultinv I) . u),u) = q1. I )
let u be Element of Quot. I; ::_thesis: ( u <> q0. I implies ( (quotmult I) . (u,((quotmultinv I) . u)) = q1. I & (quotmult I) . (((quotmultinv I) . u),u) = q1. I ) )
assume A1: u <> q0. I ; ::_thesis: ( (quotmult I) . (u,((quotmultinv I) . u)) = q1. I & (quotmult I) . (((quotmultinv I) . u),u) = q1. I )
A2: (quotmult I) . (((quotmultinv I) . u),u) = (quotmult I) . ((qmultinv u),u) by Def15
.= qmult ((qmultinv u),u) by Def13
.= q1. I by A1, Th18 ;
(quotmult I) . (u,((quotmultinv I) . u)) = (quotmult I) . (u,(qmultinv u)) by Def15
.= qmult (u,(qmultinv u)) by Def13
.= q1. I by A1, Th18 ;
hence ( (quotmult I) . (u,((quotmultinv I) . u)) = q1. I & (quotmult I) . (((quotmultinv I) . u),u) = q1. I ) by A2; ::_thesis: verum
end;
begin
definition
let I be non degenerated commutative domRing-like Ring;
func the_Field_of_Quotients I -> strict doubleLoopStr equals :: QUOFIELD:def 16
doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);
correctness
coherence
doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #) is strict doubleLoopStr ;
;
end;
:: deftheorem defines the_Field_of_Quotients QUOFIELD:def_16_:_
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I = doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);
registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> non empty strict ;
coherence
not the_Field_of_Quotients I is empty ;
end;
theorem :: QUOFIELD:30
for I being non degenerated commutative domRing-like Ring holds
( the carrier of (the_Field_of_Quotients I) = Quot. I & the addF of (the_Field_of_Quotients I) = quotadd I & the multF of (the_Field_of_Quotients I) = quotmult I & 0. (the_Field_of_Quotients I) = q0. I & 1. (the_Field_of_Quotients I) = q1. I ) ;
theorem :: QUOFIELD:31
for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of (the_Field_of_Quotients I) holds (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I)
let u, v be Element of (the_Field_of_Quotients I); ::_thesis: (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I)
reconsider s = u, t = v as Element of Quot. I ;
(quotadd I) . (u,v) = qadd (s,t) by Def12;
hence (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I) ; ::_thesis: verum
end;
theorem Th32: :: QUOFIELD:32
for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds (quotaddinv I) . u is Element of (the_Field_of_Quotients I)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of (the_Field_of_Quotients I) holds (quotaddinv I) . u is Element of (the_Field_of_Quotients I)
let u be Element of (the_Field_of_Quotients I); ::_thesis: (quotaddinv I) . u is Element of (the_Field_of_Quotients I)
reconsider s = u as Element of Quot. I ;
(quotaddinv I) . u = qaddinv s by Def14;
hence (quotaddinv I) . u is Element of (the_Field_of_Quotients I) ; ::_thesis: verum
end;
theorem :: QUOFIELD:33
for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds (quotmult I) . (u,v) is Element of (the_Field_of_Quotients I)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u, v being Element of (the_Field_of_Quotients I) holds (quotmult I) . (u,v) is Element of (the_Field_of_Quotients I)
let u, v be Element of (the_Field_of_Quotients I); ::_thesis: (quotmult I) . (u,v) is Element of (the_Field_of_Quotients I)
reconsider s = u as Element of Quot. I ;
reconsider t = v as Element of Quot. I ;
(quotmult I) . (u,v) = qmult (s,t) by Def13;
hence (quotmult I) . (u,v) is Element of (the_Field_of_Quotients I) ; ::_thesis: verum
end;
theorem :: QUOFIELD:34
for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds (quotmultinv I) . u is Element of (the_Field_of_Quotients I)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of (the_Field_of_Quotients I) holds (quotmultinv I) . u is Element of (the_Field_of_Quotients I)
let u be Element of (the_Field_of_Quotients I); ::_thesis: (quotmultinv I) . u is Element of (the_Field_of_Quotients I)
reconsider s = u as Element of Quot. I ;
(quotmultinv I) . u = qmultinv s by Def15;
hence (quotmultinv I) . u is Element of (the_Field_of_Quotients I) ; ::_thesis: verum
end;
theorem :: QUOFIELD:35
for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u + v = (quotadd I) . (u,v) ;
Lm2: for I being non degenerated commutative domRing-like Ring holds
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: ( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
A1: the_Field_of_Quotients I is right_complementable
proof
let v be Element of (the_Field_of_Quotients I); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider m = v as Element of Quot. I ;
reconsider n = (quotaddinv I) . m as Element of (the_Field_of_Quotients I) ;
take n ; :: according to ALGSTR_0:def_11 ::_thesis: v + n = 0. (the_Field_of_Quotients I)
thus v + n = 0. (the_Field_of_Quotients I) by Th28; ::_thesis: verum
end;
( ( for u, v, w being Element of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w) ) & ( for v being Element of (the_Field_of_Quotients I) holds v + (0. (the_Field_of_Quotients I)) = v ) ) by Th20, Th22;
hence ( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable ) by A1, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;
registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> right_complementable strict add-associative right_zeroed ;
coherence
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable ) by Lm2;
end;
theorem :: QUOFIELD:36
for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds - u = (quotaddinv I) . u
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of (the_Field_of_Quotients I) holds - u = (quotaddinv I) . u
let u be Element of (the_Field_of_Quotients I); ::_thesis: - u = (quotaddinv I) . u
reconsider z = (quotaddinv I) . u as Element of (the_Field_of_Quotients I) by Th32;
z + u = 0. (the_Field_of_Quotients I) by Th28;
hence - u = (quotaddinv I) . u by RLVECT_1:6; ::_thesis: verum
end;
theorem :: QUOFIELD:37
for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u * v = (quotmult I) . (u,v) ;
Lm3: for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty commutative doubleLoopStr
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: the_Field_of_Quotients I is non empty commutative doubleLoopStr
for x, y being Element of (the_Field_of_Quotients I) holds x * y = y * x by Th24;
hence the_Field_of_Quotients I is non empty commutative doubleLoopStr by GROUP_1:def_12; ::_thesis: verum
end;
registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> strict commutative ;
coherence
the_Field_of_Quotients I is commutative by Lm3;
end;
Lm4: for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: the_Field_of_Quotients I is well-unital
let x be Element of (the_Field_of_Quotients I); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (the_Field_of_Quotients I)) = x & (1. (the_Field_of_Quotients I)) * x = x )
thus ( x * (1. (the_Field_of_Quotients I)) = x & (1. (the_Field_of_Quotients I)) * x = x ) by Th25; ::_thesis: verum
end;
registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> strict well-unital ;
coherence
the_Field_of_Quotients I is well-unital by Lm4;
end;
theorem :: QUOFIELD:38
for I being non degenerated commutative domRing-like Ring holds
( 1. (the_Field_of_Quotients I) = q1. I & 0. (the_Field_of_Quotients I) = q0. I ) ;
theorem :: QUOFIELD:39
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w) by Th20;
theorem :: QUOFIELD:40
for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u + v = v + u by Th21;
theorem :: QUOFIELD:41
for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds u + (0. (the_Field_of_Quotients I)) = u by Th22;
theorem :: QUOFIELD:42
for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds (1. (the_Field_of_Quotients I)) * u = u by Th25;
theorem :: QUOFIELD:43
for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u * v = v * u ;
theorem :: QUOFIELD:44
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of (the_Field_of_Quotients I) holds (u * v) * w = u * (v * w) by Th23;
theorem Th45: :: QUOFIELD:45
for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) st u <> 0. (the_Field_of_Quotients I) holds
ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I)
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for u being Element of (the_Field_of_Quotients I) st u <> 0. (the_Field_of_Quotients I) holds
ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I)
let u be Element of (the_Field_of_Quotients I); ::_thesis: ( u <> 0. (the_Field_of_Quotients I) implies ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I) )
assume A1: u <> 0. (the_Field_of_Quotients I) ; ::_thesis: ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I)
reconsider u = u as Element of Quot. I ;
reconsider v = (quotmultinv I) . u as Element of (the_Field_of_Quotients I) ;
reconsider u = u as Element of (the_Field_of_Quotients I) ;
u * v = 1. (the_Field_of_Quotients I) by A1, Th29;
hence ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I) ; ::_thesis: verum
end;
theorem Th46: :: QUOFIELD:46
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative distributive doubleLoopStr
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: the_Field_of_Quotients I is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative distributive doubleLoopStr
A1: the_Field_of_Quotients I is almost_left_invertible
proof
let x be Element of (the_Field_of_Quotients I); :: according to ALGSTR_0:def_39 ::_thesis: ( x = 0. (the_Field_of_Quotients I) or x is left_invertible )
assume x <> 0. (the_Field_of_Quotients I) ; ::_thesis: x is left_invertible
then consider y being Element of (the_Field_of_Quotients I) such that
A2: x * y = 1. (the_Field_of_Quotients I) by Th45;
take y ; :: according to ALGSTR_0:def_27 ::_thesis: y * x = 1. (the_Field_of_Quotients I)
thus y * x = 1. (the_Field_of_Quotients I) by A2; ::_thesis: verum
end;
A3: ( q0. I <> q1. I & 0. (the_Field_of_Quotients I) = q0. I ) by Th19;
A4: ( 1. (the_Field_of_Quotients I) = q1. I & ( for x, y, z being Element of (the_Field_of_Quotients I) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ) ) by Th26, Th27;
( ( for x, y, z being Element of (the_Field_of_Quotients I) holds (x * y) * z = x * (y * z) ) & ( for u, v being Element of (the_Field_of_Quotients I) holds u + v = v + u ) ) by Th21, Th23;
hence the_Field_of_Quotients I is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative distributive doubleLoopStr by A1, A3, A4, GROUP_1:def_3, RLVECT_1:def_2, STRUCT_0:def_8, VECTSP_1:def_7; ::_thesis: verum
end;
registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> non degenerated almost_left_invertible strict Abelian associative distributive ;
coherence
( the_Field_of_Quotients I is Abelian & the_Field_of_Quotients I is associative & the_Field_of_Quotients I is distributive & the_Field_of_Quotients I is almost_left_invertible & not the_Field_of_Quotients I is degenerated ) by Th46;
end;
theorem Th47: :: QUOFIELD:47
for I being non degenerated commutative domRing-like Ring
for x being Element of (the_Field_of_Quotients I) st x <> 0. (the_Field_of_Quotients I) holds
for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: for x being Element of (the_Field_of_Quotients I) st x <> 0. (the_Field_of_Quotients I) holds
for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let x be Element of (the_Field_of_Quotients I); ::_thesis: ( x <> 0. (the_Field_of_Quotients I) implies for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v )
assume A1: x <> 0. (the_Field_of_Quotients I) ; ::_thesis: for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let a be Element of I; ::_thesis: ( a <> 0. I implies for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v )
assume A2: a <> 0. I ; ::_thesis: for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
then reconsider res = [a,a] as Element of Q. I by Def1;
XX: ( [a,a] `1 = a & [a,a] `2 = a ) ;
A3: for u being set st u in QClass. res holds
u in q1. I
proof
let u be set ; ::_thesis: ( u in QClass. res implies u in q1. I )
assume A4: u in QClass. res ; ::_thesis: u in q1. I
then reconsider u = u as Element of Q. I ;
(u `1) * a = (u `1) * (res `2) by XX
.= (u `2) * (res `1) by A4, Def4
.= (u `2) * a by XX ;
then u `1 = u `2 by A2, GCD_1:1;
hence u in q1. I by Def9; ::_thesis: verum
end;
for u being set st u in q1. I holds
u in QClass. res
proof
let u be set ; ::_thesis: ( u in q1. I implies u in QClass. res )
assume A5: u in q1. I ; ::_thesis: u in QClass. res
then reconsider u = u as Element of Q. I ;
(u `1) * (res `2) = (u `1) * a by XX
.= (u `2) * a by A5, Def9
.= (u `2) * (res `1) by XX ;
hence u in QClass. res by Def4; ::_thesis: verum
end;
then A6: q1. I = QClass. res by A3, TARSKI:1;
let u be Element of Q. I; ::_thesis: ( x = QClass. u & u = [a,(1. I)] implies for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v )
assume that
A7: x = QClass. u and
A8: u = [a,(1. I)] ; ::_thesis: for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
XY: ( [a,(1. I)] `1 = a & [a,(1. I)] `2 = 1. I ) ;
let v be Element of Q. I; ::_thesis: ( v = [(1. I),a] implies x " = QClass. v )
assume A9: v = [(1. I),a] ; ::_thesis: x " = QClass. v
YY: ( [(1. I),a] `1 = 1. I & [(1. I),a] `2 = a ) ;
pmult (u,v) = [(a * (v `1)),((u `2) * (v `2))] by A8, XY
.= [(a * (1. I)),((u `2) * (v `2))] by A9, YY
.= [(a * (1. I)),((1. I) * (v `2))] by A8, XY
.= [(a * (1. I)),((1. I) * a)] by A9, YY
.= [a,((1. I) * a)] by VECTSP_1:def_6
.= [a,a] by VECTSP_1:def_6 ;
then A10: qmult ((QClass. u),(QClass. v)) = 1. (the_Field_of_Quotients I) by A6, Th10;
reconsider y = QClass. v as Element of (the_Field_of_Quotients I) ;
reconsider y = y as Element of (the_Field_of_Quotients I) ;
qmult ((QClass. u),(QClass. v)) = x * y by A7, Def13;
hence x " = QClass. v by A1, A10, VECTSP_1:def_10; ::_thesis: verum
end;
registration
cluster non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive -> non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative right_unital well-unital distributive domRing-like for doubleLoopStr ;
coherence
for b1 being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds
( b1 is domRing-like & b1 is right_unital )
proof
let R be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: ( R is domRing-like & R is right_unital )
thus R is domRing-like ::_thesis: R is right_unital
proof
let x, y be Element of R; :: according to VECTSP_2:def_1 ::_thesis: ( not x * y = 0. R or x = 0. R or y = 0. R )
assume that
A1: x * y = 0. R and
A2: x <> 0. R ; ::_thesis: y = 0. R
x * y = x * (0. R) by A1, VECTSP_1:7;
hence y = 0. R by A2, VECTSP_1:5; ::_thesis: verum
end;
let x be Element of R; :: according to VECTSP_1:def_4 ::_thesis: x * (1. R) = x
x * (1_ R) = x by VECTSP_1:def_8;
hence x * (1. R) = x ; ::_thesis: verum
end;
end;
registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is left_unital & b1 is distributive & b1 is almost_left_invertible & not b1 is degenerated )
proof
set R = the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ;
take the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; ::_thesis: ( the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is add-associative & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is right_zeroed & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is right_complementable & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is Abelian & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is commutative & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is associative & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is left_unital & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is distributive & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is almost_left_invertible & not the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is degenerated )
thus ( the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is add-associative & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is right_zeroed & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is right_complementable & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is Abelian & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is commutative & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is associative & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is left_unital & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is distributive & the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is almost_left_invertible & not the non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr is degenerated ) ; ::_thesis: verum
end;
end;
definition
let F be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let x, y be Element of F;
funcx / y -> Element of F equals :: QUOFIELD:def 17
x * (y ");
correctness
coherence
x * (y ") is Element of F;
;
end;
:: deftheorem defines / QUOFIELD:def_17_:_
for F being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x, y being Element of F holds x / y = x * (y ");
theorem Th48: :: QUOFIELD:48
for F being non degenerated almost_left_invertible commutative Ring
for a, b, c, d being Element of F st b <> 0. F & d <> 0. F holds
(a / b) * (c / d) = (a * c) / (b * d)
proof
let F be non degenerated almost_left_invertible commutative Ring; ::_thesis: for a, b, c, d being Element of F st b <> 0. F & d <> 0. F holds
(a / b) * (c / d) = (a * c) / (b * d)
let a, b, c, d be Element of F; ::_thesis: ( b <> 0. F & d <> 0. F implies (a / b) * (c / d) = (a * c) / (b * d) )
assume A1: ( b <> 0. F & d <> 0. F ) ; ::_thesis: (a / b) * (c / d) = (a * c) / (b * d)
(a / b) * (c / d) = a * ((b ") * (c * (d "))) by GROUP_1:def_3
.= a * (((b ") * (d ")) * c) by GROUP_1:def_3
.= (a * c) * ((b ") * (d ")) by GROUP_1:def_3
.= (a * c) / (d * b) by A1, GCD_1:49 ;
hence (a / b) * (c / d) = (a * c) / (b * d) ; ::_thesis: verum
end;
theorem Th49: :: QUOFIELD:49
for F being non degenerated almost_left_invertible commutative Ring
for a, b, c, d being Element of F st b <> 0. F & d <> 0. F holds
(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
proof
let F be non degenerated almost_left_invertible commutative Ring; ::_thesis: for a, b, c, d being Element of F st b <> 0. F & d <> 0. F holds
(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
let a, b, c, d be Element of F; ::_thesis: ( b <> 0. F & d <> 0. F implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume that
A1: b <> 0. F and
A2: d <> 0. F ; ::_thesis: (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
((a * d) + (c * b)) / (b * d) = ((a * d) + (c * b)) * ((b ") * (d ")) by A1, A2, GCD_1:49
.= (((a * d) + (c * b)) * (b ")) * (d ") by GROUP_1:def_3
.= (((a * d) * (b ")) + ((c * b) * (b "))) * (d ") by VECTSP_1:def_3
.= (((a * d) * (b ")) + (c * (b * (b ")))) * (d ") by GROUP_1:def_3
.= (((a * d) * (b ")) + (c * (1. F))) * (d ") by A1, VECTSP_1:def_10
.= (((a * d) * (b ")) + c) * (d ") by VECTSP_1:def_6
.= (((a * d) * (b ")) * (d ")) + (c * (d ")) by VECTSP_1:def_3
.= ((b ") * ((a * d) * (d "))) + (c * (d ")) by GROUP_1:def_3
.= ((b ") * (a * (d * (d ")))) + (c * (d ")) by GROUP_1:def_3
.= ((b ") * (a * (1. F))) + (c * (d ")) by A2, VECTSP_1:def_10
.= ((b ") * a) + (c * (d ")) by VECTSP_1:def_6 ;
hence (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) ; ::_thesis: verum
end;
begin
definition
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attrf is RingHomomorphism means :Def18: :: QUOFIELD:def 18
( f is additive & f is multiplicative & f is unity-preserving );
end;
:: deftheorem Def18 defines RingHomomorphism QUOFIELD:def_18_:_
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingHomomorphism iff ( f is additive & f is multiplicative & f is unity-preserving ) );
registration
let R, S be non empty doubleLoopStr ;
cluster Function-like quasi_total RingHomomorphism -> unity-preserving multiplicative additive for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is RingHomomorphism holds
( b1 is additive & b1 is multiplicative & b1 is unity-preserving ) by Def18;
cluster Function-like quasi_total unity-preserving multiplicative additive -> RingHomomorphism for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is additive & b1 is multiplicative & b1 is unity-preserving holds
b1 is RingHomomorphism by Def18;
end;
definition
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attrf is RingEpimorphism means :Def19: :: QUOFIELD:def 19
( f is RingHomomorphism & rng f = the carrier of S );
attrf is RingMonomorphism means :Def20: :: QUOFIELD:def 20
( f is RingHomomorphism & f is one-to-one );
end;
:: deftheorem Def19 defines RingEpimorphism QUOFIELD:def_19_:_
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingEpimorphism iff ( f is RingHomomorphism & rng f = the carrier of S ) );
:: deftheorem Def20 defines RingMonomorphism QUOFIELD:def_20_:_
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingMonomorphism iff ( f is RingHomomorphism & f is one-to-one ) );
notation
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
synonym embedding f for RingMonomorphism ;
end;
definition
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attrf is RingIsomorphism means :Def21: :: QUOFIELD:def 21
( f is RingMonomorphism & f is RingEpimorphism );
end;
:: deftheorem Def21 defines RingIsomorphism QUOFIELD:def_21_:_
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingIsomorphism iff ( f is RingMonomorphism & f is RingEpimorphism ) );
registration
let R, S be non empty doubleLoopStr ;
cluster Function-like quasi_total RingIsomorphism -> RingEpimorphism RingMonomorphism for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is RingIsomorphism holds
( b1 is RingMonomorphism & b1 is RingEpimorphism ) by Def21;
cluster Function-like quasi_total RingEpimorphism RingMonomorphism -> RingIsomorphism for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is RingMonomorphism & b1 is RingEpimorphism holds
b1 is RingIsomorphism by Def21;
end;
theorem Th50: :: QUOFIELD:50
for R, S being Ring
for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
proof
let R, S be Ring; ::_thesis: for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
let f be Function of R,S; ::_thesis: ( f is RingHomomorphism implies f . (0. R) = 0. S )
assume A1: f is RingHomomorphism ; ::_thesis: f . (0. R) = 0. S
f . (0. R) = f . ((0. R) + (0. R)) by RLVECT_1:4
.= (f . (0. R)) + (f . (0. R)) by A1, VECTSP_1:def_20 ;
then 0. S = ((f . (0. R)) + (f . (0. R))) + (- (f . (0. R))) by RLVECT_1:def_10
.= (f . (0. R)) + ((f . (0. R)) + (- (f . (0. R)))) by RLVECT_1:def_3
.= (f . (0. R)) + (0. S) by RLVECT_1:def_10
.= f . (0. R) by RLVECT_1:4 ;
hence f . (0. R) = 0. S ; ::_thesis: verum
end;
theorem Th51: :: QUOFIELD:51
for R, S being Ring
for f being Function of R,S st f is RingMonomorphism holds
for x being Element of R holds
( f . x = 0. S iff x = 0. R )
proof
let R, S be Ring; ::_thesis: for f being Function of R,S st f is RingMonomorphism holds
for x being Element of R holds
( f . x = 0. S iff x = 0. R )
let f be Function of R,S; ::_thesis: ( f is RingMonomorphism implies for x being Element of R holds
( f . x = 0. S iff x = 0. R ) )
assume A1: f is RingMonomorphism ; ::_thesis: for x being Element of R holds
( f . x = 0. S iff x = 0. R )
then A2: f is RingHomomorphism by Def20;
let x be Element of R; ::_thesis: ( f . x = 0. S iff x = 0. R )
A3: f is one-to-one by A1, Def20;
( f . x = 0. S implies x = 0. R )
proof
assume A4: f . x = 0. S ; ::_thesis: x = 0. R
f . (0. R) = 0. S by A2, Th50;
hence x = 0. R by A3, A4, FUNCT_2:19; ::_thesis: verum
end;
hence ( f . x = 0. S iff x = 0. R ) by A2, Th50; ::_thesis: verum
end;
theorem Th52: :: QUOFIELD:52
for R, S being non degenerated almost_left_invertible commutative Ring
for f being Function of R,S st f is RingHomomorphism holds
for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) "
proof
let R, S be non degenerated almost_left_invertible commutative Ring; ::_thesis: for f being Function of R,S st f is RingHomomorphism holds
for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) "
let f be Function of R,S; ::_thesis: ( f is RingHomomorphism implies for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) " )
assume A1: f is RingHomomorphism ; ::_thesis: for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) "
let x be Element of R; ::_thesis: ( x <> 0. R implies f . (x ") = (f . x) " )
assume A2: x <> 0. R ; ::_thesis: f . (x ") = (f . x) "
A3: (f . x) * (f . (x ")) = f . ((x ") * x) by A1, GROUP_6:def_6
.= f . (1_ R) by A2, VECTSP_1:def_10
.= 1_ S by A1, GROUP_1:def_13 ;
then f . x <> 0. S by VECTSP_1:7;
hence f . (x ") = (f . x) " by A3, VECTSP_1:def_10; ::_thesis: verum
end;
theorem Th53: :: QUOFIELD:53
for R, S being non degenerated almost_left_invertible commutative Ring
for f being Function of R,S st f is RingHomomorphism holds
for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ")
proof
let R, S be non degenerated almost_left_invertible commutative Ring; ::_thesis: for f being Function of R,S st f is RingHomomorphism holds
for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ")
let f be Function of R,S; ::_thesis: ( f is RingHomomorphism implies for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ") )
assume A1: f is RingHomomorphism ; ::_thesis: for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ")
let x, y be Element of R; ::_thesis: ( y <> 0. R implies f . (x * (y ")) = (f . x) * ((f . y) ") )
assume A2: y <> 0. R ; ::_thesis: f . (x * (y ")) = (f . x) * ((f . y) ")
thus f . (x * (y ")) = (f . x) * (f . (y ")) by A1, GROUP_6:def_6
.= (f . x) * ((f . y) ") by A1, A2, Th52 ; ::_thesis: verum
end;
theorem Th54: :: QUOFIELD:54
for R, S, T being Ring
for f being Function of R,S st f is RingHomomorphism holds
for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
proof
let R, S, T be Ring; ::_thesis: for f being Function of R,S st f is RingHomomorphism holds
for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
let f be Function of R,S; ::_thesis: ( f is RingHomomorphism implies for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism )
assume A1: f is RingHomomorphism ; ::_thesis: for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
let g be Function of S,T; ::_thesis: ( g is RingHomomorphism implies g * f is RingHomomorphism )
assume A2: g is RingHomomorphism ; ::_thesis: g * f is RingHomomorphism
then A3: for x, y being Element of S holds
( g . (x + y) = (g . x) + (g . y) & g . (x * y) = (g . x) * (g . y) & g . (1_ S) = 1_ T ) by GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
A4: for x, y being Element of R holds (g * f) . (x * y) = ((g * f) . x) * ((g * f) . y)
proof
let x, y be Element of R; ::_thesis: (g * f) . (x * y) = ((g * f) . x) * ((g * f) . y)
thus (g * f) . (x * y) = g . (f . (x * y)) by FUNCT_2:15
.= g . ((f . x) * (f . y)) by A1, GROUP_6:def_6
.= (g . (f . x)) * (g . (f . y)) by A2, GROUP_6:def_6
.= ((g * f) . x) * (g . (f . y)) by FUNCT_2:15
.= ((g * f) . x) * ((g * f) . y) by FUNCT_2:15 ; ::_thesis: verum
end;
A5: for x, y being Element of R holds (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
proof
let x, y be Element of R; ::_thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by A1, VECTSP_1:def_20
.= (g . (f . x)) + (g . (f . y)) by A2, VECTSP_1:def_20
.= ((g * f) . x) + (g . (f . y)) by FUNCT_2:15
.= ((g * f) . x) + ((g * f) . y) by FUNCT_2:15 ; ::_thesis: verum
end;
for x, y being Element of R holds
( f . (x + y) = (f . x) + (f . y) & f . (x * y) = (f . x) * (f . y) & f . (1_ R) = 1_ S ) by A1, GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
then A6: (g * f) . (1. R) = 1. T by A3, FUNCT_2:15;
( 1_ R = 1. R & 1_ T = 1. T ) ;
then ( g * f is additive & g * f is multiplicative & g * f is unity-preserving ) by A6, A5, A4, GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
hence g * f is RingHomomorphism ; ::_thesis: verum
end;
theorem Th55: :: QUOFIELD:55
for R being non empty doubleLoopStr holds id R is RingHomomorphism
proof
let R be non empty doubleLoopStr ; ::_thesis: id R is RingHomomorphism
A1: for x, y being Element of R holds (id R) . (x + y) = ((id R) . x) + ((id R) . y)
proof
let x, y be Element of R; ::_thesis: (id R) . (x + y) = ((id R) . x) + ((id R) . y)
thus ((id R) . x) + ((id R) . y) = x + ((id R) . y) by FUNCT_1:18
.= x + y by FUNCT_1:18
.= (id R) . (x + y) by FUNCT_1:18 ; ::_thesis: verum
end;
A2: for x, y being Element of R holds (id R) . (x * y) = ((id R) . x) * ((id R) . y)
proof
let x, y be Element of R; ::_thesis: (id R) . (x * y) = ((id R) . x) * ((id R) . y)
thus ((id R) . x) * ((id R) . y) = x * ((id R) . y) by FUNCT_1:18
.= x * y by FUNCT_1:18
.= (id R) . (x * y) by FUNCT_1:18 ; ::_thesis: verum
end;
(id R) . (1_ R) = 1_ R by FUNCT_1:18;
then ( id R is additive & id R is multiplicative & id R is unity-preserving ) by A1, A2, GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
hence id R is RingHomomorphism ; ::_thesis: verum
end;
registration
let R be non empty doubleLoopStr ;
cluster id R -> RingHomomorphism ;
coherence
id R is RingHomomorphism by Th55;
end;
definition
let R, S be non empty doubleLoopStr ;
predR is_embedded_in S means :Def22: :: QUOFIELD:def 22
ex f being Function of R,S st f is RingMonomorphism ;
end;
:: deftheorem Def22 defines is_embedded_in QUOFIELD:def_22_:_
for R, S being non empty doubleLoopStr holds
( R is_embedded_in S iff ex f being Function of R,S st f is RingMonomorphism );
definition
let R, S be non empty doubleLoopStr ;
predR is_ringisomorph_to S means :Def23: :: QUOFIELD:def 23
ex f being Function of R,S st f is RingIsomorphism ;
symmetry
for R, S being non empty doubleLoopStr st ex f being Function of R,S st f is RingIsomorphism holds
ex f being Function of S,R st f is RingIsomorphism
proof
let R, S be non empty doubleLoopStr ; ::_thesis: ( ex f being Function of R,S st f is RingIsomorphism implies ex f being Function of S,R st f is RingIsomorphism )
given f being Function of R,S such that A1: f is RingIsomorphism ; ::_thesis: ex f being Function of S,R st f is RingIsomorphism
A2: rng f = the carrier of S by A1, Def19;
set g = f " ;
A3: f is one-to-one by A1, Def20;
A4: f is RingHomomorphism by A1, Def19;
for x, y being Element of S holds
( (f ") . (x + y) = ((f ") . x) + ((f ") . y) & (f ") . (x * y) = ((f ") . x) * ((f ") . y) & (f ") . (1_ S) = 1_ R )
proof
let x, y be Element of S; ::_thesis: ( (f ") . (x + y) = ((f ") . x) + ((f ") . y) & (f ") . (x * y) = ((f ") . x) * ((f ") . y) & (f ") . (1_ S) = 1_ R )
consider x9 being set such that
A5: x9 in the carrier of R and
A6: f . x9 = x by A2, FUNCT_2:11;
reconsider x9 = x9 as Element of R by A5;
A7: f is onto by A2, FUNCT_2:def_3;
A8: x9 = (f ") . (f . x9) by A3, FUNCT_2:26
.= (f ") . x by A3, A6, A7, TOPS_2:def_4 ;
consider y9 being set such that
A9: y9 in the carrier of R and
A10: f . y9 = y by A2, FUNCT_2:11;
reconsider y9 = y9 as Element of R by A9;
A11: y9 = (f ") . (f . y9) by A3, FUNCT_2:26
.= (f ") . y by A3, A10, A7, TOPS_2:def_4 ;
thus (f ") . (x + y) = (f ") . (f . (x9 + y9)) by A4, A6, A10, VECTSP_1:def_20
.= (f ") . (f . (x9 + y9)) by A7, A3, TOPS_2:def_4
.= ((f ") . x) + ((f ") . y) by A3, A8, A11, FUNCT_2:26 ; ::_thesis: ( (f ") . (x * y) = ((f ") . x) * ((f ") . y) & (f ") . (1_ S) = 1_ R )
thus (f ") . (x * y) = (f ") . (f . (x9 * y9)) by A4, A6, A10, GROUP_6:def_6
.= (f ") . (f . (x9 * y9)) by A7, A3, TOPS_2:def_4
.= ((f ") . x) * ((f ") . y) by A3, A8, A11, FUNCT_2:26 ; ::_thesis: (f ") . (1_ S) = 1_ R
thus (f ") . (1_ S) = (f ") . (f . (1_ R)) by A4, GROUP_1:def_13
.= (f ") . (f . (1_ R)) by A7, A3, TOPS_2:def_4
.= 1_ R by A3, FUNCT_2:26 ; ::_thesis: verum
end;
then A12: ( f " is additive & f " is multiplicative & f " is unity-preserving ) by GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
A13: rng f = [#] S by A1, Def19;
then rng (f ") = [#] R by A3, TOPS_2:49
.= the carrier of R ;
then A14: f " is RingEpimorphism by A12, Def19;
f " is one-to-one by A3, A13, TOPS_2:50;
then f " is RingMonomorphism by A12, Def20;
hence ex f being Function of S,R st f is RingIsomorphism by A14; ::_thesis: verum
end;
end;
:: deftheorem Def23 defines is_ringisomorph_to QUOFIELD:def_23_:_
for R, S being non empty doubleLoopStr holds
( R is_ringisomorph_to S iff ex f being Function of R,S st f is RingIsomorphism );
begin
definition
let I be non empty ZeroStr ;
let x, y be Element of I;
assume A1: y <> 0. I ;
func quotient (x,y) -> Element of Q. I equals :Def24: :: QUOFIELD:def 24
[x,y];
coherence
[x,y] is Element of Q. I by A1, Def1;
end;
:: deftheorem Def24 defines quotient QUOFIELD:def_24_:_
for I being non empty ZeroStr
for x, y being Element of I st y <> 0. I holds
quotient (x,y) = [x,y];
definition
let I be non degenerated commutative domRing-like Ring;
func canHom I -> Function of I,(the_Field_of_Quotients I) means :Def25: :: QUOFIELD:def 25
for x being Element of I holds it . x = QClass. (quotient (x,(1. I)));
existence
ex b1 being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b1 . x = QClass. (quotient (x,(1. I)))
proof
set f = { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ;
A1: for u being set st u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } holds
ex a, b being set st u = [a,b]
proof
let u be set ; ::_thesis: ( u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } implies ex a, b being set st u = [a,b] )
assume u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ; ::_thesis: ex a, b being set st u = [a,b]
then ex a, b being Element of I st
( u = [a,(QClass. (quotient (a,b)))] & b = 1. I ) ;
hence ex a, b being set st u = [a,b] ; ::_thesis: verum
end;
for a, b1, b2 being set st [a,b1] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } & [a,b2] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } holds
b1 = b2
proof
let a, b1, b2 be set ; ::_thesis: ( [a,b1] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } & [a,b2] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } implies b1 = b2 )
assume that
A2: [a,b1] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } and
A3: [a,b2] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ; ::_thesis: b1 = b2
consider x1, x2 being Element of I such that
A4: [a,b1] = [x1,(QClass. (quotient (x1,x2)))] and
A5: x2 = 1. I by A2;
A6: a = x1 by A4, XTUPLE_0:1;
consider y1, y2 being Element of I such that
A7: [a,b2] = [y1,(QClass. (quotient (y1,y2)))] and
A8: y2 = 1. I by A3;
A9: a = y1 by A7, XTUPLE_0:1;
reconsider a = a as Element of I by A6;
b1 = b2 by A4, A5, A7, A8, A6, A9, XTUPLE_0:1;
hence b1 = b2 ; ::_thesis: verum
end;
then reconsider f = { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } as Function by A1, FUNCT_1:def_1, RELAT_1:def_1;
A10: for x being set st x in dom f holds
x in the carrier of I
proof
let x be set ; ::_thesis: ( x in dom f implies x in the carrier of I )
assume x in dom f ; ::_thesis: x in the carrier of I
then consider y being set such that
A11: [x,y] in f by XTUPLE_0:def_12;
consider a, b being Element of I such that
A12: [x,y] = [a,(QClass. (quotient (a,b)))] and
b = 1. I by A11;
x = a by A12, XTUPLE_0:1;
hence x in the carrier of I ; ::_thesis: verum
end;
for x being set st x in the carrier of I holds
x in dom f
proof
let x be set ; ::_thesis: ( x in the carrier of I implies x in dom f )
assume x in the carrier of I ; ::_thesis: x in dom f
then reconsider x = x as Element of I ;
[x,(QClass. (quotient (x,(1. I))))] in f ;
hence x in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A13: dom f = the carrier of I by A10, TARSKI:1;
for y being set st y in rng f holds
y in the carrier of (the_Field_of_Quotients I)
proof
let y be set ; ::_thesis: ( y in rng f implies y in the carrier of (the_Field_of_Quotients I) )
assume y in rng f ; ::_thesis: y in the carrier of (the_Field_of_Quotients I)
then consider x being set such that
A14: [x,y] in f by XTUPLE_0:def_13;
consider a, b being Element of I such that
A15: [x,y] = [a,(QClass. (quotient (a,b)))] and
b = 1. I by A14;
y = QClass. (quotient (a,b)) by A15, XTUPLE_0:1;
hence y in the carrier of (the_Field_of_Quotients I) ; ::_thesis: verum
end;
then rng f c= the carrier of (the_Field_of_Quotients I) by TARSKI:def_3;
then reconsider f = f as Function of I,(the_Field_of_Quotients I) by A13, FUNCT_2:def_1, RELSET_1:4;
for x being Element of I holds f . x = QClass. (quotient (x,(1. I)))
proof
let x be Element of I; ::_thesis: f . x = QClass. (quotient (x,(1. I)))
[x,(QClass. (quotient (x,(1. I))))] in f ;
hence f . x = QClass. (quotient (x,(1. I))) by A13, FUNCT_1:def_2; ::_thesis: verum
end;
hence ex b1 being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b1 . x = QClass. (quotient (x,(1. I))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of I,(the_Field_of_Quotients I) st ( for x being Element of I holds b1 . x = QClass. (quotient (x,(1. I))) ) & ( for x being Element of I holds b2 . x = QClass. (quotient (x,(1. I))) ) holds
b1 = b2
proof
let f1, f2 be Function of I,(the_Field_of_Quotients I); ::_thesis: ( ( for x being Element of I holds f1 . x = QClass. (quotient (x,(1. I))) ) & ( for x being Element of I holds f2 . x = QClass. (quotient (x,(1. I))) ) implies f1 = f2 )
assume A16: for x being Element of I holds f1 . x = QClass. (quotient (x,(1. I))) ; ::_thesis: ( ex x being Element of I st not f2 . x = QClass. (quotient (x,(1. I))) or f1 = f2 )
assume A17: for x being Element of I holds f2 . x = QClass. (quotient (x,(1. I))) ; ::_thesis: f1 = f2
A18: for x being set st x in the carrier of I holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in the carrier of I implies f1 . x = f2 . x )
assume x in the carrier of I ; ::_thesis: f1 . x = f2 . x
then reconsider x = x as Element of I ;
f1 . x = QClass. (quotient (x,(1. I))) by A16
.= f2 . x by A17 ;
hence f1 . x = f2 . x ; ::_thesis: verum
end;
( dom f1 = the carrier of I & dom f2 = the carrier of I ) by FUNCT_2:def_1;
hence f1 = f2 by A18, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def25 defines canHom QUOFIELD:def_25_:_
for I being non degenerated commutative domRing-like Ring
for b2 being Function of I,(the_Field_of_Quotients I) holds
( b2 = canHom I iff for x being Element of I holds b2 . x = QClass. (quotient (x,(1. I))) );
theorem Th56: :: QUOFIELD:56
for I being non degenerated commutative domRing-like Ring holds canHom I is RingHomomorphism
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: canHom I is RingHomomorphism
A1: 0. I <> 1. I ;
for x, y being Element of I holds
( (canHom I) . (x + y) = ((canHom I) . x) + ((canHom I) . y) & (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
proof
reconsider res3 = [(1. I),(1. I)] as Element of Q. I by A1, Def1;
X: ( [(1. I),(1. I)] `1 = 1. I & [(1. I),(1. I)] `2 = 1. I ) ;
let x, y be Element of I; ::_thesis: ( (canHom I) . (x + y) = ((canHom I) . x) + ((canHom I) . y) & (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
reconsider t1 = quotient (x,(1. I)), t2 = quotient (y,(1. I)) as Element of Q. I ;
A2: t1 `2 = [x,(1. I)] `2 by A1, Def24
.= 1. I ;
( t1 `2 <> 0. I & t2 `2 <> 0. I ) by Th2;
then A3: (t1 `2) * (t2 `2) <> 0. I by VECTSP_2:def_1;
then reconsider sum = [(((t1 `1) * (t2 `2)) + ((t2 `1) * (t1 `2))),((t1 `2) * (t2 `2))] as Element of Q. I by Def1;
A4: t2 `1 = [y,(1. I)] `1 by A1, Def24
.= y ;
reconsider prod = [((t1 `1) * (t2 `1)),((t1 `2) * (t2 `2))] as Element of Q. I by A3, Def1;
A5: ( QClass. t1 = (canHom I) . x & QClass. t2 = (canHom I) . y ) by Def25;
A6: (quotadd I) . ((QClass. t1),(QClass. t2)) = qadd ((QClass. t1),(QClass. t2)) by Def12
.= QClass. (padd (t1,t2)) by Th9
.= QClass. sum ;
A7: t1 `1 = [x,(1. I)] `1 by A1, Def24
.= x ;
A8: t2 `2 = [y,(1. I)] `2 by A1, Def24
.= 1. I ;
then A9: sum = [((t1 `1) + ((t2 `1) * (1. I))),((1. I) * (1. I))] by A2, VECTSP_1:def_6
.= [((t1 `1) + (t2 `1)),((1. I) * (1. I))] by VECTSP_1:def_6
.= [(x + y),(1. I)] by A4, A7, VECTSP_1:def_6 ;
thus (canHom I) . (x + y) = QClass. (quotient ((x + y),(1. I))) by Def25
.= ((canHom I) . x) + ((canHom I) . y) by A1, A5, A6, A9, Def24 ; ::_thesis: ( (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
A10: (quotmult I) . ((QClass. t1),(QClass. t2)) = qmult ((QClass. t1),(QClass. t2)) by Def13
.= QClass. (pmult (t1,t2)) by Th10
.= QClass. prod ;
A11: prod = [(x * y),(1. I)] by A8, A2, A4, A7, VECTSP_1:def_6;
thus (canHom I) . (x * y) = QClass. (quotient ((x * y),(1. I))) by Def25
.= ((canHom I) . x) * ((canHom I) . y) by A1, A5, A10, A11, Def24 ; ::_thesis: (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I)
A12: for u being set st u in QClass. res3 holds
u in q1. I
proof
let u be set ; ::_thesis: ( u in QClass. res3 implies u in q1. I )
assume A13: u in QClass. res3 ; ::_thesis: u in q1. I
then reconsider u = u as Element of Q. I ;
u `1 = (u `1) * (1. I) by VECTSP_1:def_6
.= (u `1) * (res3 `2) by X
.= (u `2) * (res3 `1) by A13, Def4
.= (u `2) * (1. I) by X
.= u `2 by VECTSP_1:def_6 ;
hence u in q1. I by Def9; ::_thesis: verum
end;
for u being set st u in q1. I holds
u in QClass. res3
proof
let u be set ; ::_thesis: ( u in q1. I implies u in QClass. res3 )
assume A14: u in q1. I ; ::_thesis: u in QClass. res3
then reconsider u = u as Element of Q. I ;
(u `1) * (res3 `2) = (u `1) * (1. I) by X
.= u `1 by VECTSP_1:def_6
.= u `2 by A14, Def9
.= (u `2) * (1. I) by VECTSP_1:def_6
.= (u `2) * (res3 `1) by X ;
hence u in QClass. res3 by Def4; ::_thesis: verum
end;
then A15: q1. I = QClass. res3 by A12, TARSKI:1;
thus (canHom I) . (1_ I) = QClass. (quotient ((1. I),(1. I))) by Def25
.= 1_ (the_Field_of_Quotients I) by A1, A15, Def24 ; ::_thesis: verum
end;
then ( canHom I is additive & canHom I is multiplicative & canHom I is unity-preserving ) by GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
hence canHom I is RingHomomorphism ; ::_thesis: verum
end;
theorem Th57: :: QUOFIELD:57
for I being non degenerated commutative domRing-like Ring holds canHom I is embedding
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: canHom I is embedding
A1: 0. I <> 1. I ;
for x1, x2 being set st x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom (canHom I) & x2 in dom (canHom I) ) and
A3: (canHom I) . x1 = (canHom I) . x2 ; ::_thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of I by A2;
reconsider t1 = quotient (x1,(1. I)), t2 = quotient (x2,(1. I)) as Element of Q. I ;
A4: t1 in QClass. t1 by Th5;
QClass. t1 = (canHom I) . x2 by A3, Def25
.= QClass. t2 by Def25 ;
then A5: (t1 `1) * (t2 `2) = (t1 `2) * (t2 `1) by A4, Def4;
A6: t1 `2 = [x1,(1. I)] `2 by A1, Def24
.= 1. I ;
A7: t1 `1 = [x1,(1. I)] `1 by A1, Def24
.= x1 ;
A8: t2 `1 = [x2,(1. I)] `1 by A1, Def24
.= x2 ;
t2 `2 = [x2,(1. I)] `2 by A1, Def24
.= 1. I ;
then x1 = (t1 `2) * (t2 `1) by A5, A7, VECTSP_1:def_6
.= x2 by A6, A8, VECTSP_1:def_6 ;
hence x1 = x2 ; ::_thesis: verum
end;
then A9: canHom I is one-to-one by FUNCT_1:def_4;
canHom I is RingHomomorphism by Th56;
hence canHom I is embedding by A9, Def20; ::_thesis: verum
end;
theorem :: QUOFIELD:58
for I being non degenerated commutative domRing-like Ring holds I is_embedded_in the_Field_of_Quotients I
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: I is_embedded_in the_Field_of_Quotients I
canHom I is embedding by Th57;
hence I is_embedded_in the_Field_of_Quotients I by Def22; ::_thesis: verum
end;
theorem Th59: :: QUOFIELD:59
for F being non degenerated almost_left_invertible commutative domRing-like Ring holds F is_ringisomorph_to the_Field_of_Quotients F
proof
let F be non degenerated almost_left_invertible commutative domRing-like Ring; ::_thesis: F is_ringisomorph_to the_Field_of_Quotients F
A1: 0. F <> 1. F ;
A2: dom (canHom F) = the carrier of F by FUNCT_2:def_1;
A3: for x being set st x in the carrier of (the_Field_of_Quotients F) holds
x in rng (canHom F)
proof
let x be set ; ::_thesis: ( x in the carrier of (the_Field_of_Quotients F) implies x in rng (canHom F) )
assume x in the carrier of (the_Field_of_Quotients F) ; ::_thesis: x in rng (canHom F)
then reconsider x = x as Element of Quot. F ;
consider u being Element of Q. F such that
A4: x = QClass. u by Def5;
consider a, b being Element of F such that
A5: u = [a,b] and
A6: b <> 0. F by Def1;
Y: ( [a,b] `1 = a & [a,b] `2 = b ) ;
consider z being Element of F such that
A7: z * b = 1. F by A6, VECTSP_1:def_9;
reconsider t = [(a * z),(1. F)] as Element of Q. F by A1, Def1;
X: ( [(a * z),(1. F)] `1 = a * z & [(a * z),(1. F)] `2 = 1. F ) ;
A8: for x being set st x in QClass. t holds
x in QClass. u
proof
let x be set ; ::_thesis: ( x in QClass. t implies x in QClass. u )
assume A9: x in QClass. t ; ::_thesis: x in QClass. u
then reconsider x = x as Element of Q. F ;
x `1 = (x `1) * (1. F) by VECTSP_1:def_6
.= (x `1) * (t `2) by X
.= (x `2) * (t `1) by A9, Def4
.= (x `2) * (a * z) by X ;
then (x `1) * (u `2) = ((x `2) * (a * z)) * b by A5, Y
.= (x `2) * ((a * z) * b) by GROUP_1:def_3
.= (x `2) * (a * (1. F)) by A7, GROUP_1:def_3
.= (x `2) * a by VECTSP_1:def_6
.= (x `2) * (u `1) by A5, Y ;
hence x in QClass. u by Def4; ::_thesis: verum
end;
for x being set st x in QClass. u holds
x in QClass. t
proof
let x be set ; ::_thesis: ( x in QClass. u implies x in QClass. t )
assume A10: x in QClass. u ; ::_thesis: x in QClass. t
then reconsider x = x as Element of Q. F ;
(x `1) * (t `2) = (x `1) * (b * z) by A7, X
.= ((x `1) * b) * z by GROUP_1:def_3
.= ((x `1) * (u `2)) * z by A5, Y
.= ((x `2) * (u `1)) * z by A10, Def4
.= ((x `2) * a) * z by A5, Y
.= (x `2) * (a * z) by GROUP_1:def_3
.= (x `2) * (t `1) by X ;
hence x in QClass. t by Def4; ::_thesis: verum
end;
then A11: QClass. t = QClass. u by A8, TARSKI:1;
(canHom F) . (a * z) = QClass. (quotient ((a * z),(1. F))) by Def25
.= x by A1, A4, A11, Def24 ;
hence x in rng (canHom F) by A2, FUNCT_1:def_3; ::_thesis: verum
end;
for x being set st x in rng (canHom F) holds
x in the carrier of (the_Field_of_Quotients F) ;
then A12: rng (canHom F) = the carrier of (the_Field_of_Quotients F) by A3, TARSKI:1;
A13: canHom F is embedding by Th57;
then canHom F is RingHomomorphism by Def20;
then canHom F is RingEpimorphism by A12, Def19;
hence F is_ringisomorph_to the_Field_of_Quotients F by A13, Def23; ::_thesis: verum
end;
registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> strict right-distributive right_unital domRing-like ;
coherence
( the_Field_of_Quotients I is domRing-like & the_Field_of_Quotients I is right_unital & the_Field_of_Quotients I is right-distributive ) ;
end;
theorem :: QUOFIELD:60
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients (the_Field_of_Quotients I) is_ringisomorph_to the_Field_of_Quotients I by Th59;
definition
let I, F be non empty doubleLoopStr ;
let f be Function of I,F;
predI has_Field_of_Quotients_Pair F,f means :Def26: :: QUOFIELD:def 26
( f is RingMonomorphism & ( for F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f9 being Function of I,F9 st f9 is RingMonomorphism holds
ex h being Function of F,F9 st
( h is RingHomomorphism & h * f = f9 & ( for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h ) ) ) );
end;
:: deftheorem Def26 defines has_Field_of_Quotients_Pair QUOFIELD:def_26_:_
for I, F being non empty doubleLoopStr
for f being Function of I,F holds
( I has_Field_of_Quotients_Pair F,f iff ( f is RingMonomorphism & ( for F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f9 being Function of I,F9 st f9 is RingMonomorphism holds
ex h being Function of F,F9 st
( h is RingHomomorphism & h * f = f9 & ( for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h ) ) ) ) );
theorem :: QUOFIELD:61
for I being non degenerated commutative domRing-like Ring ex F being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ex f being Function of I,F st I has_Field_of_Quotients_Pair F,f
proof
let I be non degenerated commutative domRing-like Ring; ::_thesis: ex F being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ex f being Function of I,F st I has_Field_of_Quotients_Pair F,f
A1: now__::_thesis:_for_F9_being_non_empty_non_degenerated_right_complementable_almost_left_invertible_Abelian_add-associative_right_zeroed_associative_commutative_well-unital_distributive_doubleLoopStr_
for_f9_being_Function_of_I,F9_st_f9_is_RingMonomorphism_holds_
ex_h_being_Function_of_(the_Field_of_Quotients_I),F9_st_
(_h_is_RingHomomorphism_&_h_*_(canHom_I)_=_f9_&_(_for_h9_being_Function_of_(the_Field_of_Quotients_I),F9_st_h9_is_RingHomomorphism_&_h9_*_(canHom_I)_=_f9_holds_
h9_=_h_)_)
let F9 be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for f9 being Function of I,F9 st f9 is RingMonomorphism holds
ex h being Function of (the_Field_of_Quotients I),F9 st
( h is RingHomomorphism & h * (canHom I) = f9 & ( for h9 being Function of (the_Field_of_Quotients I),F9 st h9 is RingHomomorphism & h9 * (canHom I) = f9 holds
h9 = h ) )
let f9 be Function of I,F9; ::_thesis: ( f9 is RingMonomorphism implies ex h being Function of (the_Field_of_Quotients I),F9 st
( h is RingHomomorphism & h * (canHom I) = f9 & ( for h9 being Function of (the_Field_of_Quotients I),F9 st h9 is RingHomomorphism & h9 * (canHom I) = f9 holds
h9 = h ) ) )
set hh = { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } ;
A2: for u being set st u in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } holds
ex a, b being set st u = [a,b]
proof
let u be set ; ::_thesis: ( u in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } implies ex a, b being set st u = [a,b] )
assume u in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } ; ::_thesis: ex a, b being set st u = [a,b]
then ex a, b being Element of I st
( u = [[a,b],((f9 . a) * ((f9 . b) "))] & b <> 0. I ) ;
hence ex a, b being set st u = [a,b] ; ::_thesis: verum
end;
for a, b1, b2 being set st [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } & [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } holds
b1 = b2
proof
let a, b1, b2 be set ; ::_thesis: ( [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } & [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } implies b1 = b2 )
assume that
A3: [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } and
A4: [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } ; ::_thesis: b1 = b2
consider x1, x2 being Element of I such that
A5: [a,b1] = [[x1,x2],((f9 . x1) * ((f9 . x2) "))] and
x2 <> 0. I by A3;
consider y1, y2 being Element of I such that
A6: [a,b2] = [[y1,y2],((f9 . y1) * ((f9 . y2) "))] and
y2 <> 0. I by A4;
A7: a = [y1,y2] by A6, XTUPLE_0:1;
A8: a = [x1,x2] by A5, XTUPLE_0:1;
then A9: x2 = y2 by A7, XTUPLE_0:1;
x1 = y1 by A7, A8, XTUPLE_0:1;
then b1 = b2 by A5, A6, A9, XTUPLE_0:1;
hence b1 = b2 ; ::_thesis: verum
end;
then reconsider hh = { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } as Function by A2, FUNCT_1:def_1, RELAT_1:def_1;
A10: for x being set st x in dom hh holds
x in Q. I
proof
let x be set ; ::_thesis: ( x in dom hh implies x in Q. I )
assume x in dom hh ; ::_thesis: x in Q. I
then consider y being set such that
A11: [x,y] in hh by XTUPLE_0:def_12;
consider a, b being Element of I such that
A12: [x,y] = [[a,b],((f9 . a) * ((f9 . b) "))] and
A13: b <> 0. I by A11;
x = [a,b] by A12, XTUPLE_0:1;
hence x in Q. I by A13, Def1; ::_thesis: verum
end;
for x being set st x in Q. I holds
x in dom hh
proof
let x be set ; ::_thesis: ( x in Q. I implies x in dom hh )
assume x in Q. I ; ::_thesis: x in dom hh
then consider a, b being Element of I such that
A14: x = [a,b] and
A15: b <> 0. I by Def1;
[[a,b],((f9 . a) * ((f9 . b) "))] in hh by A15;
hence x in dom hh by A14, XTUPLE_0:def_12; ::_thesis: verum
end;
then A16: dom hh = Q. I by A10, TARSKI:1;
for y being set st y in rng hh holds
y in the carrier of F9
proof
let y be set ; ::_thesis: ( y in rng hh implies y in the carrier of F9 )
assume y in rng hh ; ::_thesis: y in the carrier of F9
then consider x being set such that
A17: [x,y] in hh by XTUPLE_0:def_13;
consider a, b being Element of I such that
A18: [x,y] = [[a,b],((f9 . a) * ((f9 . b) "))] and
b <> 0. I by A17;
y = (f9 . a) * ((f9 . b) ") by A18, XTUPLE_0:1;
hence y in the carrier of F9 ; ::_thesis: verum
end;
then rng hh c= the carrier of F9 by TARSKI:def_3;
then reconsider hh = hh as Function of (Q. I), the carrier of F9 by A16, FUNCT_2:def_1, RELSET_1:4;
set h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ;
( 0. F9 <> 1. F9 & (1. F9) * (1. F9) = 1. F9 ) by VECTSP_1:def_6;
then A19: (1. F9) " = 1. F9 by VECTSP_1:def_10;
assume A20: f9 is RingMonomorphism ; ::_thesis: ex h being Function of (the_Field_of_Quotients I),F9 st
( h is RingHomomorphism & h * (canHom I) = f9 & ( for h9 being Function of (the_Field_of_Quotients I),F9 st h9 is RingHomomorphism & h9 * (canHom I) = f9 holds
h9 = h ) )
then A21: f9 is RingHomomorphism by Def20;
A22: for v being set st v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } holds
ex a, b being set st v = [a,b]
proof
let v be set ; ::_thesis: ( v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } implies ex a, b being set st v = [a,b] )
assume v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ; ::_thesis: ex a, b being set st v = [a,b]
then ex u being Element of Q. I st
( v = [(QClass. u),(hh . u)] & 1. I = 1. I ) ;
hence ex a, b being set st v = [a,b] ; ::_thesis: verum
end;
A23: for x being Element of Q. I holds hh . x = (f9 . (x `1)) * ((f9 . (x `2)) ")
proof
let x be Element of Q. I; ::_thesis: hh . x = (f9 . (x `1)) * ((f9 . (x `2)) ")
consider a, b being Element of I such that
A24: x = [a,b] and
A25: b <> 0. I by Def1;
A26: [[a,b],((f9 . a) * ((f9 . b) "))] in hh by A25;
( [a,b] `1 = a & [a,b] `2 = b ) ;
hence hh . x = (f9 . (x `1)) * ((f9 . (x `2)) ") by A16, A24, A26, FUNCT_1:def_2; ::_thesis: verum
end;
for a, b1, b2 being set st [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } & [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } holds
b1 = b2
proof
let a, b1, b2 be set ; ::_thesis: ( [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } & [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } implies b1 = b2 )
assume that
A27: [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } and
A28: [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ; ::_thesis: b1 = b2
consider u1 being Element of Q. I such that
A29: [a,b1] = [(QClass. u1),(hh . u1)] and
1. I = 1. I by A27;
consider u2 being Element of Q. I such that
A30: [a,b2] = [(QClass. u2),(hh . u2)] and
1. I = 1. I by A28;
A31: a = QClass. u2 by A30, XTUPLE_0:1;
a = QClass. u1 by A29, XTUPLE_0:1;
then u1 in QClass. u2 by A31, Th5;
then A32: (u1 `1) * (u2 `2) = (u1 `2) * (u2 `1) by Def4;
u1 `2 <> 0. I by Th2;
then A33: f9 . (u1 `2) <> 0. F9 by A20, Th51;
u2 `2 <> 0. I by Th2;
then A34: f9 . (u2 `2) <> 0. F9 by A20, Th51;
A35: f9 is RingHomomorphism by A20, Def20;
A36: hh . u1 = (f9 . (u1 `1)) / (f9 . (u1 `2)) by A23
.= ((f9 . (u1 `1)) / (f9 . (u1 `2))) * (1. F9) by VECTSP_1:def_6
.= ((f9 . (u1 `1)) / (f9 . (u1 `2))) * ((f9 . (u2 `2)) / (f9 . (u2 `2))) by A34, VECTSP_1:def_10
.= ((f9 . (u1 `1)) * (f9 . (u2 `2))) / ((f9 . (u1 `2)) * (f9 . (u2 `2))) by A33, A34, Th48
.= (f9 . ((u1 `2) * (u2 `1))) / ((f9 . (u1 `2)) * (f9 . (u2 `2))) by A32, A35, GROUP_6:def_6
.= ((f9 . (u1 `2)) * (f9 . (u2 `1))) / ((f9 . (u1 `2)) * (f9 . (u2 `2))) by A35, GROUP_6:def_6
.= ((f9 . (u1 `2)) / (f9 . (u1 `2))) * ((f9 . (u2 `1)) / (f9 . (u2 `2))) by A33, A34, Th48
.= (1. F9) * ((f9 . (u2 `1)) * ((f9 . (u2 `2)) ")) by A33, VECTSP_1:def_10
.= (f9 . (u2 `1)) * ((f9 . (u2 `2)) ") by VECTSP_1:def_6
.= hh . u2 by A23 ;
b1 = hh . u2 by A36, A29, XTUPLE_0:1
.= b2 by A30, XTUPLE_0:1 ;
hence b1 = b2 ; ::_thesis: verum
end;
then reconsider h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } as Function by A22, FUNCT_1:def_1, RELAT_1:def_1;
A37: for x being set st x in dom h holds
x in Quot. I
proof
let x be set ; ::_thesis: ( x in dom h implies x in Quot. I )
assume x in dom h ; ::_thesis: x in Quot. I
then consider y being set such that
A38: [x,y] in h by XTUPLE_0:def_12;
consider u being Element of Q. I such that
A39: [x,y] = [(QClass. u),(hh . u)] and
1. I = 1. I by A38;
x = QClass. u by A39, XTUPLE_0:1;
hence x in Quot. I ; ::_thesis: verum
end;
for x being set st x in Quot. I holds
x in dom h
proof
let x be set ; ::_thesis: ( x in Quot. I implies x in dom h )
assume x in Quot. I ; ::_thesis: x in dom h
then consider u being Element of Q. I such that
A40: x = QClass. u by Def5;
[(QClass. u),(hh . u)] in h ;
hence x in dom h by A40, XTUPLE_0:def_12; ::_thesis: verum
end;
then A41: dom h = Quot. I by A37, TARSKI:1;
for y being set st y in rng h holds
y in the carrier of F9
proof
let y be set ; ::_thesis: ( y in rng h implies y in the carrier of F9 )
assume y in rng h ; ::_thesis: y in the carrier of F9
then consider x being set such that
A42: [x,y] in h by XTUPLE_0:def_13;
consider u being Element of Q. I such that
A43: [x,y] = [(QClass. u),(hh . u)] and
1. I = 1. I by A42;
y = hh . u by A43, XTUPLE_0:1;
hence y in the carrier of F9 ; ::_thesis: verum
end;
then rng h c= the carrier of F9 by TARSKI:def_3;
then reconsider h = h as Function of (Quot. I), the carrier of F9 by A41, FUNCT_2:def_1, RELSET_1:4;
reconsider h = h as Function of (the_Field_of_Quotients I),F9 ;
A44: for x being Element of (the_Field_of_Quotients I)
for u being Element of Q. I st x = QClass. u holds
h . x = hh . u
proof
let x be Element of (the_Field_of_Quotients I); ::_thesis: for u being Element of Q. I st x = QClass. u holds
h . x = hh . u
let u be Element of Q. I; ::_thesis: ( x = QClass. u implies h . x = hh . u )
A45: [(QClass. u),(hh . u)] in h ;
assume x = QClass. u ; ::_thesis: h . x = hh . u
hence h . x = hh . u by A41, A45, FUNCT_1:def_2; ::_thesis: verum
end;
A46: now__::_thesis:_for_h9_being_Function_of_(the_Field_of_Quotients_I),F9_st_h9_is_RingHomomorphism_&_h9_*_(canHom_I)_=_f9_holds_
h9_=_h
let h9 be Function of (the_Field_of_Quotients I),F9; ::_thesis: ( h9 is RingHomomorphism & h9 * (canHom I) = f9 implies h9 = h )
assume that
A47: h9 is RingHomomorphism and
A48: h9 * (canHom I) = f9 ; ::_thesis: h9 = h
A49: 0. I <> 1. I ;
for x being set st x in the carrier of (the_Field_of_Quotients I) holds
h9 . x = h . x
proof
let x be set ; ::_thesis: ( x in the carrier of (the_Field_of_Quotients I) implies h9 . x = h . x )
assume x in the carrier of (the_Field_of_Quotients I) ; ::_thesis: h9 . x = h . x
then reconsider x = x as Element of (the_Field_of_Quotients I) ;
reconsider x9 = x as Element of Quot. I ;
consider u being Element of Q. I such that
A50: x9 = QClass. u by Def5;
consider a, b being Element of I such that
A51: u = [a,b] and
A52: b <> 0. I by Def1;
Xu: ( [a,b] `1 = a & [a,b] `2 = b ) ;
reconsider a9 = [a,(1. I)], b9 = [b,(1. I)] as Element of Q. I by A49, Def1;
X2: ( [a,(1. I)] `1 = a & [a,(1. I)] `2 = 1. I ) ;
reconsider a99 = QClass. a9, b99 = QClass. b9 as Element of (the_Field_of_Quotients I) ;
reconsider bi = [(1. I),b] as Element of Q. I by A52, Def1;
X1: ( [(1. I),b] `1 = 1. I & [(1. I),b] `2 = b ) ;
reconsider aa = QClass. (quotient (a,(1. I))) as Element of (the_Field_of_Quotients I) ;
reconsider bb = QClass. (quotient (b,(1. I))) as Element of (the_Field_of_Quotients I) ;
reconsider bi9 = QClass. bi as Element of (the_Field_of_Quotients I) ;
A53: pmult (a9,bi) = [(a * (bi `1)),((a9 `2) * (bi `2))] by X2
.= [(a * (1. I)),((a9 `2) * (bi `2))] by X1
.= [(a * (1. I)),((1. I) * (bi `2))] by X2
.= [(a * (1. I)),((1. I) * b)] by X1
.= [a,((1. I) * b)] by VECTSP_1:def_6
.= [a,b] by VECTSP_1:def_6 ;
A54: b99 <> 0. (the_Field_of_Quotients I)
proof
A55: b9 in b99 by Th5;
assume A56: b99 = 0. (the_Field_of_Quotients I) ; ::_thesis: contradiction
b = [b,(1. I)] `1
.= 0. I by A56, A55, Def8 ;
hence contradiction by A52; ::_thesis: verum
end;
A57: h . x = hh . u by A44, A50
.= ((h9 * (canHom I)) . (u `1)) * ((f9 . (u `2)) ") by A23, A48
.= (h9 . ((canHom I) . (u `1))) * (((h9 * (canHom I)) . (u `2)) ") by A48, FUNCT_2:15
.= (h9 . ((canHom I) . (u `1))) * ((h9 . ((canHom I) . (u `2))) ") by FUNCT_2:15 ;
A58: h9 . ((quotmult I) . (a99,bi9)) = h9 . (qmult ((QClass. a9),(QClass. bi))) by Def13
.= h9 . (QClass. (pmult (a9,bi))) by Th10 ;
(h9 . ((canHom I) . (u `1))) * ((h9 . ((canHom I) . (u `2))) ") = (h9 . ((canHom I) . a)) * ((h9 . ((canHom I) . (u `2))) ") by A51, Xu
.= (h9 . aa) * ((h9 . ((canHom I) . (u `2))) ") by Def25
.= (h9 . a99) * ((h9 . ((canHom I) . (u `2))) ") by A49, Def24
.= (h9 . a99) * ((h9 . ((canHom I) . b)) ") by A51, Xu
.= (h9 . a99) * ((h9 . bb) ") by Def25
.= (h9 . a99) * ((h9 . b99) ") by A49, Def24
.= h9 . (a99 * (b99 ")) by A47, A54, Th53 ;
hence h9 . x = h . x by A50, A51, A52, A57, A54, A58, A53, Th47; ::_thesis: verum
end;
hence h9 = h by FUNCT_2:12; ::_thesis: verum
end;
A59: 1_ F9 = 1. F9 ;
for x, y being Element of (the_Field_of_Quotients I) holds
( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 )
proof
let x, y be Element of (the_Field_of_Quotients I); ::_thesis: ( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 )
reconsider x = x, y = y as Element of Quot. I ;
A60: 0. F9 <> 1. F9 ;
consider u being Element of Q. I such that
A61: x = QClass. u by Def5;
A62: u `2 <> 0. I by Th2;
then A63: f9 . (u `2) <> 0. F9 by A20, Th51;
consider v being Element of Q. I such that
A64: y = QClass. v by Def5;
A65: v `2 <> 0. I by Th2;
then A66: f9 . (v `2) <> 0. F9 by A20, Th51;
A67: (u `2) * (v `2) <> 0. I by A62, A65, VECTSP_2:def_1;
then reconsider t = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] as Element of Q. I by Def1;
Xt: ( [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] `1 = ((u `1) * (v `2)) + ((v `1) * (u `2)) & [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
reconsider x = x, y = y as Element of (the_Field_of_Quotients I) ;
reconsider x9 = x, y9 = y as Element of Quot. I ;
A68: h . (qadd (x9,y9)) = h . (QClass. (padd (u,v))) by A61, A64, Th9
.= h . (QClass. t) ;
A69: (h . x) + (h . y) = (hh . u) + (h . y) by A44, A61
.= (hh . u) + (hh . v) by A44, A64
.= ((f9 . (u `1)) * ((f9 . (u `2)) ")) + (hh . v) by A23
.= ((f9 . (u `1)) / (f9 . (u `2))) + ((f9 . (v `1)) / (f9 . (v `2))) by A23
.= (((f9 . (u `1)) * (f9 . (v `2))) + ((f9 . (v `1)) * (f9 . (u `2)))) / ((f9 . (u `2)) * (f9 . (v `2))) by A63, A66, Th49
.= ((f9 . ((u `1) * (v `2))) + ((f9 . (v `1)) * (f9 . (u `2)))) / ((f9 . (u `2)) * (f9 . (v `2))) by A21, GROUP_6:def_6
.= ((f9 . ((u `1) * (v `2))) + (f9 . ((v `1) * (u `2)))) / ((f9 . (u `2)) * (f9 . (v `2))) by A21, GROUP_6:def_6
.= ((f9 . ((u `1) * (v `2))) + (f9 . ((v `1) * (u `2)))) * ((f9 . ((u `2) * (v `2))) ") by A21, GROUP_6:def_6
.= (f9 . (((u `1) * (v `2)) + ((v `1) * (u `2)))) * ((f9 . ((u `2) * (v `2))) ") by A21, VECTSP_1:def_20
.= (f9 . (t `1)) * ((f9 . ((u `2) * (v `2))) ") by Xt
.= (f9 . (t `1)) * ((f9 . (t `2)) ") by Xt
.= hh . t by A23 ;
A70: h . (QClass. t) = hh . t by A44;
reconsider t = [((u `1) * (v `1)),((u `2) * (v `2))] as Element of Q. I by A67, Def1;
Xt: ( [((u `1) * (v `1)),((u `2) * (v `2))] `1 = (u `1) * (v `1) & [((u `1) * (v `1)),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
A71: (h . x) * (h . y) = (hh . u) * (h . y) by A44, A61
.= (hh . u) * (hh . v) by A44, A64
.= ((f9 . (u `1)) * ((f9 . (u `2)) ")) * (hh . v) by A23
.= ((f9 . (u `1)) / (f9 . (u `2))) * ((f9 . (v `1)) / (f9 . (v `2))) by A23
.= ((f9 . (u `1)) * (f9 . (v `1))) / ((f9 . (u `2)) * (f9 . (v `2))) by A63, A66, Th48
.= (f9 . ((u `1) * (v `1))) / ((f9 . (u `2)) * (f9 . (v `2))) by A21, GROUP_6:def_6
.= (f9 . ((u `1) * (v `1))) * ((f9 . ((u `2) * (v `2))) ") by A21, GROUP_6:def_6
.= (f9 . (t `1)) * ((f9 . ((u `2) * (v `2))) ") by Xt
.= (f9 . (t `1)) * ((f9 . (t `2)) ") by Xt
.= hh . t by A23 ;
reconsider x9 = x, y9 = y as Element of Quot. I ;
A72: h . (qmult (x9,y9)) = h . (QClass. (pmult (u,v))) by A61, A64, Th10
.= h . (QClass. t) ;
A73: h . (QClass. t) = hh . t by A44;
0. I <> 1. I ;
then reconsider t = [(1. I),(1. I)] as Element of Q. I by Def1;
Xt: ( [(1. I),(1. I)] `1 = 1. I & [(1. I),(1. I)] `2 = 1. I ) ;
A74: for u being set st u in QClass. t holds
u in q1. I
proof
let u be set ; ::_thesis: ( u in QClass. t implies u in q1. I )
assume A75: u in QClass. t ; ::_thesis: u in q1. I
then reconsider u = u as Element of Q. I ;
u `1 = (u `1) * (1. I) by VECTSP_1:def_6
.= (u `1) * (t `2) by Xt
.= (u `2) * (t `1) by A75, Def4
.= (u `2) * (1. I) by Xt
.= u `2 by VECTSP_1:def_6 ;
hence u in q1. I by Def9; ::_thesis: verum
end;
for u being set st u in q1. I holds
u in QClass. t
proof
let u be set ; ::_thesis: ( u in q1. I implies u in QClass. t )
assume A76: u in q1. I ; ::_thesis: u in QClass. t
then reconsider u = u as Element of Q. I ;
(u `1) * (t `2) = (u `1) * (1. I) by Xt
.= u `1 by VECTSP_1:def_6
.= u `2 by A76, Def9
.= (u `2) * (1. I) by VECTSP_1:def_6
.= (u `2) * (t `1) by Xt ;
hence u in QClass. t by Def4; ::_thesis: verum
end;
then q1. I = QClass. t by A74, TARSKI:1;
then h . (1_ (the_Field_of_Quotients I)) = hh . t by A44
.= (f9 . (t `1)) * ((f9 . (t `2)) ") by A23
.= (f9 . (1. I)) * ((f9 . (t `2)) ") by Xt
.= (f9 . (1. I)) * ((f9 . (1. I)) ") by Xt
.= (1. F9) * ((f9 . (1_ I)) ") by A21, A59, GROUP_1:def_13
.= (1. F9) * ((1_ F9) ") by A21, GROUP_1:def_13
.= 1_ F9 by A60, VECTSP_1:def_10 ;
hence ( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 ) by A69, A68, A70, A71, A72, A73, Def12, Def13; ::_thesis: verum
end;
then A77: ( h is additive & h is multiplicative & h is unity-preserving ) by GROUP_1:def_13, GROUP_6:def_6, VECTSP_1:def_20;
A78: for x being set st x in dom f9 holds
( x in dom (canHom I) & (canHom I) . x in dom h )
proof
let x be set ; ::_thesis: ( x in dom f9 implies ( x in dom (canHom I) & (canHom I) . x in dom h ) )
assume x in dom f9 ; ::_thesis: ( x in dom (canHom I) & (canHom I) . x in dom h )
then reconsider x = x as Element of I ;
dom h = the carrier of (the_Field_of_Quotients I) by FUNCT_2:def_1;
then ( x in the carrier of I & (canHom I) . x in dom h ) ;
hence ( x in dom (canHom I) & (canHom I) . x in dom h ) by FUNCT_2:def_1; ::_thesis: verum
end;
A79: 0. I <> 1. I ;
A80: for x being set st x in dom f9 holds
f9 . x = h . ((canHom I) . x)
proof
let x be set ; ::_thesis: ( x in dom f9 implies f9 . x = h . ((canHom I) . x) )
assume x in dom f9 ; ::_thesis: f9 . x = h . ((canHom I) . x)
then reconsider x = x as Element of I ;
reconsider u = [x,(1. I)] as Element of Q. I by A79, Def1;
Xu: ( [x,(1. I)] `1 = x & [x,(1. I)] `2 = 1. I ) ;
reconsider u9 = QClass. u as Element of (the_Field_of_Quotients I) ;
h . ((canHom I) . x) = h . (QClass. (quotient (x,(1. I)))) by Def25
.= h . u9 by Def24
.= hh . u by A44
.= (f9 . (u `1)) * ((f9 . (u `2)) ") by A23
.= (f9 . (u `1)) * ((f9 . (1_ I)) ") by Xu
.= (f9 . (u `1)) * (1_ F9) by A21, A19, GROUP_1:def_13
.= f9 . (u `1) by VECTSP_1:def_6
.= f9 . x by Xu ;
hence f9 . x = h . ((canHom I) . x) ; ::_thesis: verum
end;
for x being set st x in dom (canHom I) & (canHom I) . x in dom h holds
x in dom f9
proof
let x be set ; ::_thesis: ( x in dom (canHom I) & (canHom I) . x in dom h implies x in dom f9 )
assume that
A81: x in dom (canHom I) and
(canHom I) . x in dom h ; ::_thesis: x in dom f9
reconsider x = x as Element of I by A81;
x in the carrier of I ;
hence x in dom f9 by FUNCT_2:def_1; ::_thesis: verum
end;
then h * (canHom I) = f9 by A78, A80, FUNCT_1:10;
hence ex h being Function of (the_Field_of_Quotients I),F9 st
( h is RingHomomorphism & h * (canHom I) = f9 & ( for h9 being Function of (the_Field_of_Quotients I),F9 st h9 is RingHomomorphism & h9 * (canHom I) = f9 holds
h9 = h ) ) by A77, A46; ::_thesis: verum
end;
canHom I is embedding by Th57;
then I has_Field_of_Quotients_Pair the_Field_of_Quotients I, canHom I by A1, Def26;
hence ex F being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ex f being Function of I,F st I has_Field_of_Quotients_Pair F,f ; ::_thesis: verum
end;
theorem :: QUOFIELD:62
for I being commutative domRing-like Ring
for F, F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f being Function of I,F
for f9 being Function of I,F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 holds
F is_ringisomorph_to F9
proof
let I be commutative domRing-like Ring; ::_thesis: for F, F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f being Function of I,F
for f9 being Function of I,F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 holds
F is_ringisomorph_to F9
let F, F9 be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for f being Function of I,F
for f9 being Function of I,F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 holds
F is_ringisomorph_to F9
let f be Function of I,F; ::_thesis: for f9 being Function of I,F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 holds
F is_ringisomorph_to F9
let f9 be Function of I,F9; ::_thesis: ( I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 implies F is_ringisomorph_to F9 )
assume that
A1: I has_Field_of_Quotients_Pair F,f and
A2: I has_Field_of_Quotients_Pair F9,f9 ; ::_thesis: F is_ringisomorph_to F9
A3: (id F9) * f9 = f9 by FUNCT_2:17;
f is RingMonomorphism by A1, Def26;
then consider h2 being Function of F9,F such that
A5: ( h2 is RingHomomorphism & h2 * f9 = f ) and
for h9 being Function of F9,F st h9 is RingHomomorphism & h9 * f9 = f holds
h9 = h2 by A2, Def26;
consider h3 being Function of F,F such that
h3 is RingHomomorphism and
h3 * f = f and
A6: for h9 being Function of F,F st h9 is RingHomomorphism & h9 * f = f holds
h9 = h3 by A1, Def26;
A7: (id F) * f = f by FUNCT_2:17;
f9 is RingMonomorphism by A2, Def26;
then consider h1 being Function of F,F9 such that
A9: h1 is RingHomomorphism and
A10: h1 * f = f9 and
for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h1 by A1, Def26;
( (h2 * h1) * f = f & h2 * h1 is RingHomomorphism ) by A9, A10, A5, Th54, RELAT_1:36;
then A11: h2 * h1 = h3 by A6
.= id the carrier of F by A7, A6 ;
consider h3 being Function of F9,F9 such that
h3 is RingHomomorphism and
h3 * f9 = f9 and
A12: for h9 being Function of F9,F9 st h9 is RingHomomorphism & h9 * f9 = f9 holds
h9 = h3 by A2, Def26;
( (h1 * h2) * f9 = f9 & h1 * h2 is RingHomomorphism ) by A9, A10, A5, Th54, RELAT_1:36;
then h1 * h2 = h3 by A12
.= id the carrier of F9 by A3, A12 ;
then rng h1 = the carrier of F9 by FUNCT_2:18;
then A13: h1 is RingEpimorphism by A9, Def19;
h1 is one-to-one by A11, FUNCT_2:31;
then h1 is RingMonomorphism by A9, Def20;
hence F is_ringisomorph_to F9 by A13, Def23; ::_thesis: verum
end;