let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: ex y, z being Element of G st y + z = z
A1: now :: thesis: for x, y being Element of G holds - (x + y) = - ((- (((- (x + y)) + (- x)) + y)) + y)
let x, y be Element of G; :: thesis: - (x + y) = - ((- (((- (x + y)) + (- x)) + y)) + y)
thus - (x + y) = - ((- ((- ((- x) + y)) + (- (x + y)))) + (- (((- x) + y) + (- (x + y))))) by Def5
.= - (y + (- (((- x) + y) + (- (x + y))))) by Def5
.= - ((- (((- (x + y)) + (- x)) + y)) + y) by LATTICES:def 5 ; :: thesis: verum
end;
A2: now :: thesis: for x, y being Element of G holds - ((- x) + y) = - ((- (((- ((- x) + y)) + x) + y)) + y)
let x, y be Element of G; :: thesis: - ((- x) + y) = - ((- (((- ((- x) + y)) + x) + y)) + y)
thus - ((- x) + y) = - ((- ((- (x + y)) + (- ((- x) + y)))) + (- ((x + y) + (- ((- x) + y))))) by Def5
.= - (y + (- ((x + y) + (- ((- x) + y))))) by Def5
.= - ((- (((- ((- x) + y)) + x) + y)) + y) by LATTICES:def 5 ; :: thesis: verum
end;
A3: now :: thesis: for x, y being Element of G holds y = - ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y)))
let x, y be Element of G; :: thesis: y = - ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y)))
thus y = - ((- ((- (((- ((- x) + y)) + x) + y)) + y)) + (- ((((- ((- x) + y)) + x) + y) + y))) by Def5
.= - ((- ((- x) + y)) + (- ((((- ((- x) + y)) + x) + y) + y))) by A2
.= - ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) by LATTICES:def 5 ; :: thesis: verum
end;
A4: now :: thesis: for x, y, z being Element of G holds z = - ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z)))
let x, y, z be Element of G; :: thesis: z = - ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z)))
thus z = - ((- ((- ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y)))) + z)) + (- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z))) by Def5
.= - ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z))) by A3 ; :: thesis: verum
end;
A5: now :: thesis: for x, y, z being Element of G holds - (y + z) = - ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z)
let x, y, z be Element of G; :: thesis: - (y + z) = - ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z)
set k = ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z;
thus - (y + z) = - ((- ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z)))) + (- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z) + (- (y + z))))) by Def5
.= - (z + (- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z) + (- (y + z))))) by A4
.= - ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) by LATTICES:def 5 ; :: thesis: verum
end;
A6: now :: thesis: for x, y, z, u being Element of G holds u = - ((- ((- (y + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u)))
let x, y, z, u be Element of G; :: thesis: u = - ((- ((- (y + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u)))
set k = (- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z;
thus u = - ((- ((- ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u))) by Def5
.= - ((- ((- (y + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u))) by A5 ; :: thesis: verum
end;
A7: now :: thesis: for x, y, z, v being Element of G holds - ((- ((Double v) + v)) + v) = - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + (Double v)) + v) + (- ((- ((Double v) + v)) + v)))))
let x, y, z, v be Element of G; :: thesis: - ((- ((Double v) + v)) + v) = - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + (Double v)) + v) + (- ((- ((Double v) + v)) + v)))))
set k = - ((- ((Double v) + v)) + v);
set l = (- ((- ((Double v) + v)) + v)) + (Double v);
set v5 = ((Double v) + (Double v)) + v;
A8: - (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v))) = - ((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + (- ((Double v) + v))) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) by A1
.= - ((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- ((Double v) + v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) by LATTICES:def 5 ;
thus - ((- ((Double v) + v)) + v) = - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- ((((- (((- ((- ((Double v) + v)) + v)) + ((Double v) + v)) + (Double v))) + (- ((- ((Double v) + v)) + v))) + (- (v + (Double v)))) + (Double v))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by A6
.= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- ((((- ((((Double v) + v) + (- ((- ((Double v) + v)) + v))) + (Double v))) + (- ((- ((Double v) + v)) + v))) + (Double v)) + (- (v + (Double v))))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def 5
.= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- (((- ((((Double v) + v) + (- ((- ((Double v) + v)) + v))) + (Double v))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- (v + (Double v))))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def 5
.= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- (v + (Double v))))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def 5
.= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- ((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- (v + (Double v))))) + ((- ((- ((Double v) + v)) + v)) + (Double v))))) by LATTICES:def 5
.= - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + v) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by A8, LATTICES:def 5
.= - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + (Double v)) + v) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def 5 ; :: thesis: verum
end;
A9: now :: thesis: for x being Element of G holds - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((Double x) + x)
let x be Element of G; :: thesis: - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((Double x) + x)
set k = (- ((- ((Double x) + x)) + x)) + (- ((Double x) + x));
set l = - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x));
A10: - ((Double x) + x) = - ((- (((- (((- ((- ((Double x) + x)) + x)) + ((Double x) + x)) + (Double x))) + (- ((- ((Double x) + x)) + x))) + (- ((Double x) + x)))) + (- (x + (- ((Double x) + x))))) by A4
.= - ((- ((- (((- ((- ((Double x) + x)) + x)) + ((Double x) + x)) + (Double x))) + ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))))) + (- (x + (- ((Double x) + x))))) by LATTICES:def 5
.= - ((- ((- ((- ((- ((Double x) + x)) + x)) + (((Double x) + x) + (Double x)))) + ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))))) + (- (x + (- ((Double x) + x))))) by LATTICES:def 5
.= - ((- ((- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x))) + ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))))) + (- (x + (- ((Double x) + x))))) by LATTICES:def 5 ;
- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((- ((- ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x))))) + (- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))))) by Def5
.= - ((- ((- ((Double x) + x)) + x)) + (- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))))) by A7 ;
hence - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((Double x) + x) by A10; :: thesis: verum
end;
A11: now :: thesis: for x being Element of G holds x = - ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)))
let x be Element of G; :: thesis: x = - ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)))
A12: - ((- ((Double x) + x)) + x) = - ((- (((- ((- ((Double x) + x)) + x)) + ((Double x) + x)) + x)) + x) by A2
.= - ((- ((- ((- ((Double x) + x)) + x)) + (((Double x) + x) + x))) + x) by LATTICES:def 5
.= - ((- ((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x)))) + x) by LATTICES:def 5 ;
thus x = - ((- ((- ((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x)))) + x)) + (- (((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x))) + x))) by Def5
.= - ((- ((- ((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x)))) + x)) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))) by LATTICES:def 5
.= - ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) by A9, A12 ; :: thesis: verum
end;
A13: now :: thesis: for x, y being Element of G holds y = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y)) + (- (x + y)))
let x, y be Element of G; :: thesis: y = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y)) + (- (x + y)))
thus y = - ((- ((- ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)))) + y)) + (- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y))) by Def5
.= - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y)) + (- (x + y))) by A11 ; :: thesis: verum
end;
A14: now :: thesis: for x being Element of G holds (- ((- ((Double x) + x)) + x)) + (Double x) = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- ((Double x) + x)))
let x be Element of G; :: thesis: (- ((- ((Double x) + x)) + x)) + (Double x) = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- ((Double x) + x)))
thus (- ((- ((Double x) + x)) + x)) + (Double x) = - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- (((Double x) + x) + ((- ((- ((Double x) + x)) + x)) + (Double x))))) by Def5
.= - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + x) + (Double x))))) by LATTICES:def 5
.= - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))) by LATTICES:def 5
.= - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- ((Double x) + x))) by A9
.= - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- ((Double x) + x))) by LATTICES:def 5 ; :: thesis: verum
end;
A15: now :: thesis: for x, y being Element of G holds Double x = (- ((- ((Double x) + x)) + x)) + (Double x)
let x, y be Element of G; :: thesis: Double x = (- ((- ((Double x) + x)) + x)) + (Double x)
thus Double x = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- (x + (Double x)))) by A13
.= (- ((- ((Double x) + x)) + x)) + (Double x) by A14 ; :: thesis: verum
end;
set x = the Element of G;
set c = Double the Element of G;
set d = - ((- ((Double the Element of G) + the Element of G)) + the Element of G);
take - ((- ((Double the Element of G) + the Element of G)) + the Element of G) ; :: thesis: ex z being Element of G st (- ((- ((Double the Element of G) + the Element of G)) + the Element of G)) + z = z
take Double the Element of G ; :: thesis: (- ((- ((Double the Element of G) + the Element of G)) + the Element of G)) + (Double the Element of G) = Double the Element of G
thus (- ((- ((Double the Element of G) + the Element of G)) + the Element of G)) + (Double the Element of G) = Double the Element of G by A15; :: thesis: verum