let R be finite Skew-Field; :: thesis: for s being Element of R st s is Element of (MultGroup R) holds
dim (VectSp_over_center s) divides dim (VectSp_over_center R)
let s be Element of R; :: thesis: ( s is Element of (MultGroup R) implies dim (VectSp_over_center s) divides dim (VectSp_over_center R) )
assume A1: s is Element of (MultGroup R) ; :: thesis: dim (VectSp_over_center s) divides dim (VectSp_over_center R)
set n = dim (VectSp_over_center R);
set ns = dim (VectSp_over_center s);
set q = card the carrier of (center R);
A2: ( dim (VectSp_over_center R) in NAT & dim (VectSp_over_center s) in NAT ) by ORDINAL1:def 13;
A3: ( 0 < dim (VectSp_over_center R) & 0 < dim (VectSp_over_center s) ) by Th33, Th35;
A4: 1 < card the carrier of (center R) by Th21;
0 < (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) by PREPOWER:13;
then 0 + 1 < ((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) + 1 by XREAL_1:10;
then A5: 1 <= (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) by NAT_1:13;
0 < (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by PREPOWER:13;
then 0 + 1 < ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) + 1 by XREAL_1:10;
then 1 <= (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by NAT_1:13;
then A6: ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) -' 1 by XREAL_1:235;
((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) - 1 = ((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) -' 1 by A5, XREAL_1:235;
hence dim (VectSp_over_center s) divides dim (VectSp_over_center R) by A1, A2, A3, A4, A6, Th3, Th36; :: thesis: verum