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;
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))) )
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;
( 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)))
;
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 ( ( ((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 ) )per cases
( ((a `1) * (b `2)) + ((b `1) * (a `2)) = 0. I or ((a `1) * (b `2)) + ((b `1) * (a `2)) <> 0. I )
;
case A14:
((a `1) * (b `2)) + ((b `1) * (a `2)) <> 0. I
;
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))
;
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
.=
(z `2) * (t `1)
;
hence
z in QClass. t
by Def4;
verum end; end; end;
hence
z in QClass. t
;
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; verum