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