let L be Field; :: thesis: for m being Element of NAT
for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM x,m) * (VM (x " ),m) = (VM (x " ),m) * (VM x,m)
let m be Element of NAT ; :: thesis: for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM x,m) * (VM (x " ),m) = (VM (x " ),m) * (VM x,m)
let x be Element of L; :: thesis: ( m > 0 & x is_primitive_root_of_degree m implies (VM x,m) * (VM (x " ),m) = (VM (x " ),m) * (VM x,m) )
assume that
A1: 0 < m and
A2: x is_primitive_root_of_degree m ; :: thesis: (VM x,m) * (VM (x " ),m) = (VM (x " ),m) * (VM x,m)
x <> 0. L by A2, Th30;
then (VM (x " ),m) * (VM x,m) = (VM (x " ),m) * (VM ((x " ) " ),m) by VECTSP_1:73
.= (emb m,L) * (1. L,m) by A1, A2, Th31, Th39 ;
hence (VM x,m) * (VM (x " ),m) = (VM (x " ),m) * (VM x,m) by A1, A2, Th39; :: thesis: verum