let R be finite Skew-Field; 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; ( 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)
; 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
by ORDINAL1:def 12;
A3:
dim (VectSp_over_center s) in NAT
by ORDINAL1:def 12;
A4:
0 < dim (VectSp_over_center s)
by Th34;
A5:
1 < card the carrier of (center R)
by Th20;
0 < (card the carrier of (center R)) |^ (dim (VectSp_over_center s))
by PREPOWER:6;
then
0 + 1 < ((card the carrier of (center R)) |^ (dim (VectSp_over_center s))) + 1
by XREAL_1:8;
then A6:
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:6;
then
0 + 1 < ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) + 1
by XREAL_1:8;
then
1 <= (card the carrier of (center R)) |^ (dim (VectSp_over_center R))
by NAT_1:13;
then A7:
((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:233;
((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 A6, XREAL_1:233;
hence
dim (VectSp_over_center s) divides dim (VectSp_over_center R)
by A1, A2, A3, A4, A5, A7, Th3, Th35; verum