let p be Prime; :: thesis: for g2, a, b, c, d being Element of (GF p) st g2 = 2 mod p holds
((a * c) + (b * d)) |^ 2 = (((a |^ 2) * (c |^ 2)) + ((((g2 * a) * b) * c) * d)) + ((b |^ 2) * (d |^ 2))
let g2, a, b, c, d be Element of (GF p); :: thesis: ( g2 = 2 mod p implies ((a * c) + (b * d)) |^ 2 = (((a |^ 2) * (c |^ 2)) + ((((g2 * a) * b) * c) * d)) + ((b |^ 2) * (d |^ 2)) )
assume A1: g2 = 2 mod p ; :: thesis: ((a * c) + (b * d)) |^ 2 = (((a |^ 2) * (c |^ 2)) + ((((g2 * a) * b) * c) * d)) + ((b |^ 2) * (d |^ 2))
thus ((a * c) + (b * d)) |^ 2 = (((a * c) |^ 2) + ((g2 * (a * c)) * (b * d))) + ((b * d) |^ 2) by A1, Th25
.= (((a |^ 2) * (c |^ 2)) + ((g2 * (a * c)) * (b * d))) + ((b * d) |^ 2) by BINOM:9
.= (((a |^ 2) * (c |^ 2)) + ((g2 * (a * c)) * (b * d))) + ((b |^ 2) * (d |^ 2)) by BINOM:9
.= (((a |^ 2) * (c |^ 2)) + (g2 * ((a * c) * (b * d)))) + ((b |^ 2) * (d |^ 2)) by GROUP_1:def 3
.= (((a |^ 2) * (c |^ 2)) + (g2 * (((a * c) * b) * d))) + ((b |^ 2) * (d |^ 2)) by GROUP_1:def 3
.= (((a |^ 2) * (c |^ 2)) + (g2 * (((a * b) * c) * d))) + ((b |^ 2) * (d |^ 2)) by GROUP_1:def 3
.= (((a |^ 2) * (c |^ 2)) + ((((g2 * a) * b) * c) * d)) + ((b |^ 2) * (d |^ 2)) by Th11 ; :: thesis: verum