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
0 < m and
A1: x is_primitive_root_of_degree m ; :: thesis: (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))
x <> 0. L by A1, Th30;
then (VM ((x "),m)) * (VM (x,m)) = (VM ((x "),m)) * (VM (((x ") "),m)) by VECTSP_1:24
.= (emb (m,L)) * (1. (L,m)) by A1, Th31, Th39 ;
hence (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) by A1, Th39; :: thesis: verum