:: VECTSP_1 semantic presentation
defpred S1[ Element of REAL , set ] means a2 = - a1;
:: deftheorem Def1 VECTSP_1:def 1 :
canceled;
:: deftheorem Def2 VECTSP_1:def 2 :
canceled;
:: deftheorem Def3 VECTSP_1:def 3 :
canceled;
:: deftheorem Def4 VECTSP_1:def 4 :
canceled;
:: deftheorem Def5 VECTSP_1:def 5 :
canceled;
:: deftheorem Def6 defines G_Real VECTSP_1:def 6 :
theorem Th1: :: VECTSP_1:1
canceled;
theorem Th2: :: VECTSP_1:2
canceled;
theorem Th3: :: VECTSP_1:3
canceled;
theorem Th4: :: VECTSP_1:4
canceled;
theorem Th5: :: VECTSP_1:5
canceled;
theorem Th6: :: VECTSP_1:6
theorem Th7: :: VECTSP_1:7
:: deftheorem Def7 VECTSP_1:def 7 :
canceled;
:: deftheorem Def8 VECTSP_1:def 8 :
canceled;
:: deftheorem Def9 defines 1_ VECTSP_1:def 9 :
:: deftheorem Def10 VECTSP_1:def 10 :
canceled;
:: deftheorem Def11 defines right-distributive VECTSP_1:def 11 :
:: deftheorem Def12 defines left-distributive VECTSP_1:def 12 :
:: deftheorem Def13 defines right_unital VECTSP_1:def 13 :
:: deftheorem Def14 VECTSP_1:def 14 :
canceled;
:: deftheorem Def15 defines F_Real VECTSP_1:def 15 :
:: deftheorem Def16 VECTSP_1:def 16 :
canceled;
:: deftheorem Def17 VECTSP_1:def 17 :
canceled;
:: deftheorem Def18 defines distributive VECTSP_1:def 18 :
:: deftheorem Def19 defines left_unital VECTSP_1:def 19 :
:: deftheorem Def20 defines Field-like VECTSP_1:def 20 :
:: deftheorem Def21 defines degenerated VECTSP_1:def 21 :
set c1 = F_Real ;
Lemma9:
1. F_Real = 1
Lemma10:
for b1 being non empty doubleLoopStr st b1 is distributive holds
( b1 is right-distributive & b1 is left-distributive )
theorem Th8: :: VECTSP_1:8
canceled;
theorem Th9: :: VECTSP_1:9
canceled;
theorem Th10: :: VECTSP_1:10
canceled;
theorem Th11: :: VECTSP_1:11
canceled;
theorem Th12: :: VECTSP_1:12
canceled;
theorem Th13: :: VECTSP_1:13
canceled;
theorem Th14: :: VECTSP_1:14
canceled;
theorem Th15: :: VECTSP_1:15
canceled;
theorem Th16: :: VECTSP_1:16
canceled;
theorem Th17: :: VECTSP_1:17
canceled;
theorem Th18: :: VECTSP_1:18
canceled;
theorem Th19: :: VECTSP_1:19
canceled;
theorem Th20: :: VECTSP_1:20
theorem Th21: :: VECTSP_1:21
theorem Th22: :: VECTSP_1:22
theorem Th23: :: VECTSP_1:23
canceled;
theorem Th24: :: VECTSP_1:24
canceled;
theorem Th25: :: VECTSP_1:25
canceled;
theorem Th26: :: VECTSP_1:26
canceled;
theorem Th27: :: VECTSP_1:27
canceled;
theorem Th28: :: VECTSP_1:28
canceled;
theorem Th29: :: VECTSP_1:29
canceled;
theorem Th30: :: VECTSP_1:30
canceled;
theorem Th31: :: VECTSP_1:31
canceled;
theorem Th32: :: VECTSP_1:32
canceled;
theorem Th33: :: VECTSP_1:33
:: deftheorem Def22 defines " VECTSP_1:def 22 :
:: deftheorem Def23 defines / VECTSP_1:def 23 :
theorem Th34: :: VECTSP_1:34
canceled;
theorem Th35: :: VECTSP_1:35
canceled;
theorem Th36: :: VECTSP_1:36
theorem Th37: :: VECTSP_1:37
canceled;
theorem Th38: :: VECTSP_1:38
canceled;
theorem Th39: :: VECTSP_1:39
theorem Th40: :: VECTSP_1:40
theorem Th41: :: VECTSP_1:41
theorem Th42: :: VECTSP_1:42
theorem Th43: :: VECTSP_1:43
theorem Th44: :: VECTSP_1:44
theorem Th45: :: VECTSP_1:45
:: deftheorem Def24 defines * VECTSP_1:def 24 :
:: deftheorem Def25 defines comp VECTSP_1:def 25 :
E19:
now
let c2 be non
empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c3 be
Function of
[:the carrier of c2,the carrier of c2:],the
carrier of
c2;
set c4 =
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #);
for
b1,
b2,
b3 being
Element of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #) holds
(
b1 + b2 = b2 + b1 &
(b1 + b2) + b3 = b1 + (b2 + b3) &
b1 + (0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #)) = b1 & ex
b4 being
Element of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #) st
b1 + b4 = 0. VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #) )
proof
let c5,
c6,
c7 be
Element of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #);
reconsider c8 =
c5,
c9 =
c6,
c10 =
c7 as
Element of
c2 ;
thus c5 + c6 =
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
c6
by RLVECT_1:5
.=
c9 + c8
by RLVECT_1:5
.=
the
add of
c2 . c9,
c8
by RLVECT_1:5
.=
c6 + c5
by RLVECT_1:5
;
thus (c5 + c6) + c7 =
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. (c5 + c6),
c7
by RLVECT_1:5
.=
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. (the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c6),
c7
by RLVECT_1:5
.=
the
add of
c2 . (c8 + c9),
c10
by RLVECT_1:5
.=
(c8 + c9) + c10
by RLVECT_1:5
.=
c8 + (c9 + c10)
by RLVECT_1:def 6
.=
the
add of
c2 . c8,
(c9 + c10)
by RLVECT_1:5
.=
the
add of
c2 . c8,
(the add of c2 . c9,c10)
by RLVECT_1:5
.=
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
(c6 + c7)
by RLVECT_1:5
.=
c5 + (c6 + c7)
by RLVECT_1:5
;
thus c5 + (0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #)) =
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
(0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #))
by RLVECT_1:5
.=
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,the
Zero of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
.=
c8 + (0. c2)
by RLVECT_1:5
.=
c5
by RLVECT_1:10
;
consider c11 being
Element of
c2 such that E20:
c8 + c11 = 0. c2
by RLVECT_1:def 8;
reconsider c12 =
c11 as
Element of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #) ;
take
c12
;
thus c5 + c12 =
the
add of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
c12
by RLVECT_1:5
.=
c8 + c11
by RLVECT_1:5
.=
0. VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
by E20
;
end;
hence
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #) is
AbGroup
by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;
end;
E20:
now
let c2 be non
empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c3 be
Function of
[:the carrier of c2,the carrier of c2:],the
carrier of
c2;
assume E21:
c3 = the
mult of
c2
;
set c4 =
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #);
let c5,
c6 be
Element of
c2;
let c7,
c8 be
Element of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #);
reconsider c9 =
c7,
c10 =
c8 as
Element of
c2 ;
thus c5 * (c7 + c8) =
the
lmult of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
(c7 + c8)
.=
c3 . c5,
(the add of c2 . c9,c10)
by RLVECT_1:5
.=
c3 . c5,
(c9 + c10)
by RLVECT_1:5
.=
c5 * (c9 + c10)
by E21
.=
(c5 * c9) + (c5 * c10)
by Def18
.=
the
add of
c2 . (c5 * c9),
(c5 * c10)
by RLVECT_1:5
.=
the
add of
c2 . (c3 . c5,c9),
(c5 * c10)
by E21
.=
the
add of
c2 . (the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c7),
(the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c8)
by E21
.=
the
add of
c2 . (c5 * c7),
(c5 * c8)
.=
(c5 * c7) + (c5 * c8)
by RLVECT_1:5
;
thus (c5 + c6) * c7 =
the
lmult of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. (c5 + c6),
c7
.=
(c5 + c6) * c9
by E21
.=
(c5 * c9) + (c6 * c9)
by Def18
.=
the
add of
c2 . (c5 * c9),
(c6 * c9)
by RLVECT_1:5
.=
the
add of
c2 . (c3 . c5,c9),
(c6 * c9)
by E21
.=
the
add of
c2 . (the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c7),
(the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c6,c7)
by E21
.=
the
add of
c2 . (c5 * c7),
(c6 * c7)
.=
(c5 * c7) + (c6 * c7)
by RLVECT_1:5
;
thus (c5 * c6) * c7 =
the
lmult of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. (c5 * c6),
c7
.=
(c5 * c6) * c9
by E21
.=
c5 * (c6 * c9)
by GROUP_1:def 4
.=
c3 . c5,
(c6 * c9)
by E21
.=
the
lmult of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
(the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c6,c7)
by E21
.=
the
lmult of
VectSpStr(# the
carrier of
c2,the
add of
c2,the
Zero of
c2,
c3 #)
. c5,
(c6 * c7)
.=
c5 * (c6 * c7)
;
thus (1. c2) * c7 =
c3 . (1. c2),
c9
.=
(1. c2) * c9
by E21
.=
c7
by Def19
;
end;
:: deftheorem Def26 defines VectSp-like VECTSP_1:def 26 :
theorem Th46: :: VECTSP_1:46
canceled;
theorem Th47: :: VECTSP_1:47
canceled;
theorem Th48: :: VECTSP_1:48
canceled;
theorem Th49: :: VECTSP_1:49
canceled;
theorem Th50: :: VECTSP_1:50
canceled;
theorem Th51: :: VECTSP_1:51
canceled;
theorem Th52: :: VECTSP_1:52
canceled;
theorem Th53: :: VECTSP_1:53
canceled;
theorem Th54: :: VECTSP_1:54
canceled;
theorem Th55: :: VECTSP_1:55
canceled;
theorem Th56: :: VECTSP_1:56
canceled;
theorem Th57: :: VECTSP_1:57
canceled;
theorem Th58: :: VECTSP_1:58
canceled;
theorem Th59: :: VECTSP_1:59
theorem Th60: :: VECTSP_1:60
theorem Th61: :: VECTSP_1:61
canceled;
theorem Th62: :: VECTSP_1:62
canceled;
theorem Th63: :: VECTSP_1:63
Lemma23:
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - (b3 + (- b2)) = b2 - b3
Lemma24:
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - ((- b2) - b3) = b3 + b2
theorem Th64: :: VECTSP_1:64
theorem Th65: :: VECTSP_1:65
theorem Th66: :: VECTSP_1:66
theorem Th67: :: VECTSP_1:67
theorem Th68: :: VECTSP_1:68
theorem Th69: :: VECTSP_1:69
theorem Th70: :: VECTSP_1:70
theorem Th71: :: VECTSP_1:71
canceled;
theorem Th72: :: VECTSP_1:72
canceled;
theorem Th73: :: VECTSP_1:73
theorem Th74: :: VECTSP_1:74
theorem Th75: :: VECTSP_1:75
canceled;
theorem Th76: :: VECTSP_1:76
canceled;
theorem Th77: :: VECTSP_1:77
canceled;
theorem Th78: :: VECTSP_1:78
:: deftheorem Def27 VECTSP_1:def 27 :
canceled;
:: deftheorem Def28 defines Fanoian VECTSP_1:def 28 :
:: deftheorem Def29 defines Fanoian VECTSP_1:def 29 :
theorem Th79: :: VECTSP_1:79
canceled;
theorem Th80: :: VECTSP_1:80
canceled;
theorem Th81: :: VECTSP_1:81
theorem Th82: :: VECTSP_1:82
canceled;
theorem Th83: :: VECTSP_1:83
canceled;
theorem Th84: :: VECTSP_1:84
theorem Th85: :: VECTSP_1:85
canceled;
theorem Th86: :: VECTSP_1:86
theorem Th87: :: VECTSP_1:87
theorem Th88: :: VECTSP_1:88
for
b1 being
Field for
b2,
b3,
b4 being
Element of
b1 holds
( (
b2 <> 0. b1 &
(b2 * b4) - b3 = 0. b1 implies
b4 = b3 * (b2 " ) ) & (
b2 <> 0. b1 &
b3 - (b4 * b2) = 0. b1 implies
b4 = b3 * (b2 " ) ) )
theorem Th89: :: VECTSP_1:89
theorem Th90: :: VECTSP_1:90
theorem Th91: :: VECTSP_1:91
canceled;
theorem Th92: :: VECTSP_1:92
theorem Th93: :: VECTSP_1:93
theorem Th94: :: VECTSP_1:94