let n be Nat; for K being Field
for a being Element of K
for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let K be Field; for a being Element of K
for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let a be Element of K; for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let v, v1, v2 be Vector of (n -VectSp_over K); for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let t, t1, t2 be Element of n -tuples_on the carrier of K; ( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
A1:
addLoopStr(# the carrier of (n -VectSp_over K), the addF of (n -VectSp_over K), the ZeroF of (n -VectSp_over K) #) = n -Group_over K
by PRVECT_1:def 5;
A2:
n -Group_over K = addLoopStr(# (n -tuples_on the carrier of K),(product ( the addF of K,n)),(n |-> (0. K)) #)
by PRVECT_1:def 3;
hence
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) )
by A1; ( ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
thus
( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 )
by A2, A1, PRVECT_1:def 1; ( t = v implies a * t = a * v )
assume A3:
t = v
; a * t = a * v
rng t c= the carrier of K
by RELAT_1:def 19;
then A4:
(id the carrier of K) * t = t
by RELAT_1:53;
thus a * v =
(n -Mult_over K) . (a,v)
by PRVECT_1:def 5
.=
the multF of K [;] (a,t)
by A3, PRVECT_1:def 4
.=
a * t
by A4, FUNCOP_1:34
; verum