:: The canonical formulae
:: by Andrzej Trybulec
::
:: Received July 4, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: HILBERT3:1
theorem :: HILBERT3:2
theorem Th3: :: HILBERT3:3
theorem Th4: :: HILBERT3:4
theorem Th5: :: HILBERT3:5
theorem Th6: :: HILBERT3:6
theorem Th7: :: HILBERT3:7
theorem Th8: :: HILBERT3:8
theorem Th9: :: HILBERT3:9
theorem Th10: :: HILBERT3:10
for
a,
b,
x,
y,
x',
y' being
set st
a <> b &
a,
b --> x,
y = a,
b --> x',
y' holds
(
x = x' &
y = y' )
theorem Th11: :: HILBERT3:11
theorem Th12: :: HILBERT3:12
theorem Th13: :: HILBERT3:13
for
a,
b,
c,
d being
set st
a <> b holds
(a,b --> c,d) * (a,b --> b,a) = a,
b --> d,
c
theorem Th14: :: HILBERT3:14
theorem Th15: :: HILBERT3:15
theorem Th16: :: HILBERT3:16
theorem :: HILBERT3:17
theorem Th18: :: HILBERT3:18
theorem :: HILBERT3:19
theorem Th20: :: HILBERT3:20
theorem Th21: :: HILBERT3:21
theorem :: HILBERT3:22
canceled;
theorem Th23: :: HILBERT3:23
theorem Th24: :: HILBERT3:24
theorem Th25: :: HILBERT3:25
definition
let A,
B be non
empty set ;
let P be
Permutation of
A;
let Q be
Function of
B,
B;
func P => Q -> Function of
Funcs A,
B,
Funcs A,
B means :
Def1:
:: HILBERT3:def 1
for
f being
Function of
A,
B holds
it . f = (Q * f) * (P " );
existence
ex b1 being Function of Funcs A,B, Funcs A,B st
for f being Function of A,B holds b1 . f = (Q * f) * (P " )
uniqueness
for b1, b2 being Function of Funcs A,B, Funcs A,B st ( for f being Function of A,B holds b1 . f = (Q * f) * (P " ) ) & ( for f being Function of A,B holds b2 . f = (Q * f) * (P " ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines => HILBERT3:def 1 :
theorem Th26: :: HILBERT3:26
theorem Th27: :: HILBERT3:27
theorem Th28: :: HILBERT3:28
definition
let V be
SetValuation;
func SetVal V -> ManySortedSet of
HP-WFF means :
Def2:
:: HILBERT3:def 2
(
it . VERUM = 1 & ( for
n being
Element of
NAT holds
it . (prop n) = V . n ) & ( for
p,
q being
Element of
HP-WFF holds
(
it . (p '&' q) = [:(it . p),(it . q):] &
it . (p => q) = Funcs (it . p),
(it . q) ) ) );
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs (b1 . p),(b1 . q) ) ) )
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs (b1 . p),(b1 . q) ) ) & b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs (b2 . p),(b2 . q) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines SetVal HILBERT3:def 2 :
:: deftheorem defines SetVal HILBERT3:def 3 :
theorem :: HILBERT3:29
theorem :: HILBERT3:30
theorem :: HILBERT3:31
theorem :: HILBERT3:32
registration
let V be
SetValuation;
let p,
q,
r be
Element of
HP-WFF ;
cluster Function-yielding M5(
SetVal V,
(p => q),
SetVal V,
(p => r));
existence
ex b1 being Function of SetVal V,(p => q), SetVal V,(p => r) st b1 is Function-yielding
cluster Function-yielding Element of
SetVal V,
(p => (q => r));
existence
ex b1 being Element of SetVal V,(p => (q => r)) st b1 is Function-yielding
end;
:: deftheorem Def4 defines Permutation HILBERT3:def 4 :
definition
let V be
SetValuation;
let P be
Permutation of
V;
func Perm P -> ManySortedFunction of
SetVal V,
SetVal V means :
Def5:
:: HILBERT3:def 5
(
it . VERUM = id 1 & ( for
n being
Element of
NAT holds
it . (prop n) = P . n ) & ( for
p,
q being
Element of
HP-WFF ex
p' being
Permutation of
SetVal V,
p ex
q' being
Permutation of
SetVal V,
q st
(
p' = it . p &
q' = it . q &
it . (p '&' q) = [:p',q':] &
it . (p => q) = p' => q' ) ) );
existence
ex b1 being ManySortedFunction of SetVal V, SetVal V st
( b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = [:p',q':] & b1 . (p => q) = p' => q' ) ) )
uniqueness
for b1, b2 being ManySortedFunction of SetVal V, SetVal V st b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = [:p',q':] & b1 . (p => q) = p' => q' ) ) & b2 . VERUM = id 1 & ( for n being Element of NAT holds b2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b2 . p & q' = b2 . q & b2 . (p '&' q) = [:p',q':] & b2 . (p => q) = p' => q' ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines Perm HILBERT3:def 5 :
:: deftheorem defines Perm HILBERT3:def 6 :
theorem Th33: :: HILBERT3:33
theorem :: HILBERT3:34
theorem Th35: :: HILBERT3:35
theorem Th36: :: HILBERT3:36
theorem Th37: :: HILBERT3:37
theorem Th38: :: HILBERT3:38
theorem Th39: :: HILBERT3:39
theorem Th40: :: HILBERT3:40
:: deftheorem Def7 defines canonical HILBERT3:def 7 :
theorem Th41: :: HILBERT3:41
theorem Th42: :: HILBERT3:42
theorem Th43: :: HILBERT3:43
theorem Th44: :: HILBERT3:44
theorem Th45: :: HILBERT3:45
theorem Th46: :: HILBERT3:46
theorem :: HILBERT3:47
:: deftheorem Def8 defines pseudo-canonical HILBERT3:def 8 :
theorem :: HILBERT3:48
theorem :: HILBERT3:49
theorem :: HILBERT3:50
theorem :: HILBERT3:51
theorem :: HILBERT3:52
theorem :: HILBERT3:53
theorem Th54: :: HILBERT3:54
theorem :: HILBERT3:55