let L be Field; 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 ; 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; ( 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
; (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; verum