:: The canonical formulae
:: by Andrzej Trybulec
::
:: Received July 4, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

registration
let m, n be non zero Nat;
cluster(0,n) --> (m,0) ->  one-to-one ;
coherence
 (0,n) --> (m,0) is one-to-one
proofend;
cluster(n,0) --> (0,m) ->  one-to-one ;
coherence
 (n,0) --> (0,m) is one-to-one
proofend;
end;

theorem :: HILBERT3:1
for i being Integer holds
( i is even iff i - 1 is odd ) ;

theorem :: HILBERT3:2
for i being Integer holds
( i is odd iff i - 1 is even ) ;

theorem Th3: :: HILBERT3:3
for X being trivial set
for x being set st x in X holds
for f being Function of X,X holds x is_a_fixpoint_of f
proofend;

theorem Th4: :: HILBERT3:4
for f being Function-yielding Function holds SubFuncs (rng f) = rng f
proofend;

theorem Th5: :: HILBERT3:5
for A, B, x being set
for f being Function st x in A & f in Funcs (A,B) holds
f . x in B
proofend;

theorem Th6: :: HILBERT3:6
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A,(Funcs (B,C)) holds doms f = A --> B
proofend;

theorem :: HILBERT3:7
for x being set holds {} . x = {} ;

theorem Th8: :: HILBERT3:8
for X being set
for A being Subset of X holds ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X)
proofend;

theorem Th9: :: HILBERT3:9
for X being set
for A being Subset of X holds ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X)
proofend;

theorem Th10: :: HILBERT3:10
for a, b, x, y, x9, y9 being set st a <> b &amp; (a,b) --> (x,y) = (a,b) --> (x9,y9) holds
( x = x9 &amp; y = y9 )
proofend;

theorem Th11: :: HILBERT3:11
for a, b, x, y, X, Y being set st a <> b &amp; x in X &amp; y in Y holds
(a,b) --> (x,y) in product ((a,b) --> (X,Y))
proofend;

theorem Th12: :: HILBERT3:12
for D being non empty set
for f being Function of 2,D ex d1, d2 being Element of D st f = (0,1) --> (d1,d2)
proofend;

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)
proofend;

theorem Th14: :: HILBERT3:14
for a, b, c, d being set
for f being Function st a <> b &amp; c in dom f &amp; d in dom f holds
f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d))
proofend;

theorem Th15: :: HILBERT3:15
(0,1) --> (1,0) is Permutation of 2
proofend;

begin

registration
let f, g be one-to-one Function;
cluster[:f,g:] ->  one-to-one ;
coherence
 [:f,g:] is one-to-one
proofend;
end;

theorem Th16: :: HILBERT3:16
for A, B being non empty set
for C, D being set
for f being Function of C,A
for g being Function of D,B holds (pr1 (A,B)) * [:f,g:] = f * (pr1 (C,D))
proofend;

theorem Th17: :: HILBERT3:17
for A, B being non empty set
for C, D being set
for f being Function of C,A
for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D))
proofend;

theorem :: HILBERT3:18
for g being Function holds {} .. g = {}
proofend;

theorem Th19: :: HILBERT3:19
for f being Function-yielding Function
for g, h being Function holds (f .. g) * h = (f * h) .. (g * h)
proofend;

theorem :: HILBERT3:20
for C being set
for A being non empty set
for f being Function of A,(Funcs ({},C))
for g being Function of A,{} holds rng (f .. g) = {{}}
proofend;

theorem Th21: :: HILBERT3:21
for A, B, C being set st ( B = {} implies A = {} ) holds
for f being Function of A,(Funcs (B,C))
for g being Function of A,B holds rng (f .. g) c= C
proofend;

theorem Th22: :: HILBERT3:22
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A,(Funcs (B,C)) holds dom (Frege f) = Funcs (A,B)
proofend;

theorem Th23: :: HILBERT3:23
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C)
proofend;

theorem Th24: :: HILBERT3:24
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C))
proofend;

begin

registration
let A, B be set ;
let P be Permutation of A;
let Q be Permutation of B;
cluster[:P,Q:] ->  bijective for Function of [:A,B:],[:A,B:];
coherence
 for b1 being Function of [:A,B:],[:A,B:] st b1 = [:P,Q:] holds
b1 is bijective
proofend;
end;

theorem :: HILBERT3:25
for A, B being set
for P being Permutation of A
for Q being Permutation of B holds [:P,Q:] is bijective ;

definition
let A, B be non empty set ;
let P be Permutation of A;
let Q be Function of B,B;
funcP => 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 ")
proofend;
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 ") ) &amp; ( for f being Function of A,B holds b2 . f = (Q * f) * (P ") ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines => HILBERT3:def_1_:_
 for A, B being non empty set
for P being Permutation of A
for Q being Function of B,B
for b5 being Function of (Funcs (A,B)),(Funcs (A,B)) holds
( b5 = P => Q iff for f being Function of A,B holds b5 . f = (Q * f) * (P ") );

registration
let A, B be non empty set ;
let P be Permutation of A;
let Q be Permutation of B;
clusterP => Q ->  bijective ;
coherence
 P => Q is bijective
proofend;
end;

theorem Th26: :: HILBERT3:26
for A, B being non empty set
for P being Permutation of A
for Q being Permutation of B
for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P
proofend;

theorem Th27: :: HILBERT3:27
for A, B being non empty set
for P being Permutation of A
for Q being Permutation of B holds (P => Q) " = (P ") => (Q ")
proofend;

theorem Th28: :: HILBERT3:28
for A, B, C being non empty set
for f being Function of A,(Funcs (B,C))
for g being Function of A,B
for P being Permutation of B
for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
proofend;

begin

definition
mode SetValuation is V19() ManySortedSet of NAT ;
end;

definition
let V be SetValuation;
func SetVal V ->  ManySortedSet of HP-WFF  means :Def2: :: HILBERT3:def 2
( it . VERUM = 1 &amp; ( for n being Element of NAT holds it . (prop n) = V . n ) &amp; ( for p, q being Element of HP-WFF holds
( it . (p '&amp;' q) = [:(it . p),(it . q):] &amp; it . (p => q) = Funcs ((it . p),(it . q)) ) ) );
existence
 ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 &amp; ( for n being Element of NAT holds b1 . (prop n) = V . n ) &amp; ( for p, q being Element of HP-WFF holds
( b1 . (p '&amp;' q) = [:(b1 . p),(b1 . q):] &amp; b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 &amp; ( for n being Element of NAT holds b1 . (prop n) = V . n ) &amp; ( for p, q being Element of HP-WFF holds
( b1 . (p '&amp;' q) = [:(b1 . p),(b1 . q):] &amp; b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) &amp; b2 . VERUM = 1 &amp; ( for n being Element of NAT holds b2 . (prop n) = V . n ) &amp; ( for p, q being Element of HP-WFF holds
( b2 . (p '&amp;' q) = [:(b2 . p),(b2 . q):] &amp; b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines SetVal HILBERT3:def_2_:_
 for V being SetValuation
for b2 being ManySortedSet of HP-WFF holds
( b2 = SetVal V iff ( b2 . VERUM = 1 &amp; ( for n being Element of NAT holds b2 . (prop n) = V . n ) &amp; ( for p, q being Element of HP-WFF holds
( b2 . (p '&amp;' q) = [:(b2 . p),(b2 . q):] &amp; b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) ) );

definition
let V be SetValuation;
let p be Element of HP-WFF ;
func SetVal (V,p) ->  set  equals :: HILBERT3:def 3
(SetVal V) . p;
correctness
coherence
(SetVal V) . p is set ;
;
end;

:: deftheorem  defines SetVal HILBERT3:def_3_:_
 for V being SetValuation
for p being Element of HP-WFF holds SetVal (V,p) = (SetVal V) . p;

registration
let V be SetValuation;
let p be Element of HP-WFF ;
cluster SetVal (V,p) ->  non empty ;
coherence
 not SetVal (V,p) is empty
proofend;
end;

theorem :: HILBERT3:29
for V being SetValuation holds SetVal (V,VERUM) = 1 by Def2;

theorem :: HILBERT3:30
for n being Element of NAT
for V being SetValuation holds SetVal (V,(prop n)) = V . n by Def2;

theorem :: HILBERT3:31
for p, q being Element of HP-WFF
for V being SetValuation holds SetVal (V,(p '&amp;' q)) = [:(SetVal (V,p)),(SetVal (V,q)):] by Def2;

theorem :: HILBERT3:32
for p, q being Element of HP-WFF
for V being SetValuation holds SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2;

registration
let V be SetValuation;
let p, q be Element of HP-WFF ;
cluster SetVal (V,(p => q)) ->  functional ;
coherence
 SetVal (V,(p => q)) is functional
proofend;
end;

registration
let V be SetValuation;
let p, q, r be Element of HP-WFF ;
cluster  ->  Function-yielding for Element of SetVal (V,(p => (q => r)));
coherence
 for b1 being Element of SetVal (V,(p => (q => r))) holds b1 is Function-yielding
proofend;
end;

registration
let V be SetValuation;
let p, q, r be Element of HP-WFF ;
cluster non empty Relation-like SetVal (V,(p => q)) -defined SetVal (V,(p => r)) -valued Function-like total quasi_total Function-yielding V55() for Element of bool [:(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
proofend;
cluster Relation-like Function-like Function-yielding V55() for Element of SetVal (V,(p => (q => r)));
existence
 ex b1 being Element of SetVal (V,(p => (q => r))) st b1 is Function-yielding
proofend;
end;

begin

definition
let V be SetValuation;
mode Permutation of V ->  Function means :Def4: :: HILBERT3:def 4
( dom it = NAT &amp; ( for n being Element of NAT holds it . n is Permutation of (V . n) ) );
existence
 ex b1 being Function st
( dom b1 = NAT &amp; ( for n being Element of NAT holds b1 . n is Permutation of (V . n) ) )
proofend;
end;

:: deftheorem Def4 defines Permutation HILBERT3:def_4_:_
 for V being SetValuation
for b2 being Function holds
( b2 is Permutation of V iff ( dom b2 = NAT &amp; ( for n being Element of NAT holds b2 . n is Permutation of (V . n) ) ) );

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 &amp; ( for n being Element of NAT holds it . (prop n) = P . n ) &amp; ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = it . p &amp; q9 = it . q &amp; it . (p '&amp;' q) = [:p9,q9:] &amp; it . (p => q) = p9 => q9 ) ) );
existence
 ex b1 being ManySortedFunction of SetVal V, SetVal V st
( b1 . VERUM = id 1 &amp; ( for n being Element of NAT holds b1 . (prop n) = P . n ) &amp; ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b1 . p &amp; q9 = b1 . q &amp; b1 . (p '&amp;' q) = [:p9,q9:] &amp; b1 . (p => q) = p9 => q9 ) ) )
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of SetVal V, SetVal V st b1 . VERUM = id 1 &amp; ( for n being Element of NAT holds b1 . (prop n) = P . n ) &amp; ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b1 . p &amp; q9 = b1 . q &amp; b1 . (p '&amp;' q) = [:p9,q9:] &amp; b1 . (p => q) = p9 => q9 ) ) &amp; b2 . VERUM = id 1 &amp; ( for n being Element of NAT holds b2 . (prop n) = P . n ) &amp; ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b2 . p &amp; q9 = b2 . q &amp; b2 . (p '&amp;' q) = [:p9,q9:] &amp; b2 . (p => q) = p9 => q9 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Perm HILBERT3:def_5_:_
 for V being SetValuation
for P being Permutation of V
for b3 being ManySortedFunction of SetVal V, SetVal V holds
( b3 = Perm P iff ( b3 . VERUM = id 1 &amp; ( for n being Element of NAT holds b3 . (prop n) = P . n ) &amp; ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b3 . p &amp; q9 = b3 . q &amp; b3 . (p '&amp;' q) = [:p9,q9:] &amp; b3 . (p => q) = p9 => q9 ) ) ) );

definition
let V be SetValuation;
let P be Permutation of V;
let p be Element of HP-WFF ;
func Perm (P,p) ->  Function of (SetVal (V,p)),(SetVal (V,p)) equals :: HILBERT3:def 6
(Perm P) . p;
correctness
coherence
(Perm P) . p is Function of (SetVal (V,p)),(SetVal (V,p));
;
end;

:: deftheorem  defines Perm HILBERT3:def_6_:_
 for V being SetValuation
for P being Permutation of V
for p being Element of HP-WFF holds Perm (P,p) = (Perm P) . p;

theorem Th33: :: HILBERT3:33
for V being SetValuation
for P being Permutation of V holds Perm (P,VERUM) = id (SetVal (V,VERUM))
proofend;

theorem :: HILBERT3:34
for n being Element of NAT
for V being SetValuation
for P being Permutation of V holds Perm (P,(prop n)) = P . n by Def5;

theorem Th35: :: HILBERT3:35
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V holds Perm (P,(p '&amp;' q)) = [:(Perm (P,p)),(Perm (P,q)):]
proofend;

theorem Th36: :: HILBERT3:36
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for p9 being Permutation of (SetVal (V,p))
for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) &amp; q9 = Perm (P,q) holds
Perm (P,(p => q)) = p9 => q9
proofend;

registration
let V be SetValuation;
let P be Permutation of V;
let p be Element of HP-WFF ;
cluster Perm (P,p) ->  bijective ;
coherence
 Perm (P,p) is bijective
proofend;
end;

theorem Th37: :: HILBERT3:37
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds (Perm (P,(p => q))) . g = ((Perm (P,q)) * g) * ((Perm (P,p)) ")
proofend;

theorem Th38: :: HILBERT3:38
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p))
proofend;

theorem Th39: :: HILBERT3:39
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for f, g being Function of (SetVal (V,p)),(SetVal (V,q)) st f = (Perm (P,(p => q))) . g holds
(Perm (P,q)) * g = f * (Perm (P,p))
proofend;

theorem Th40: :: HILBERT3:40
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for x being set st x is_a_fixpoint_of Perm (P,p) holds
for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds
f . x is_a_fixpoint_of Perm (P,q)
proofend;

begin

definition
let p be Element of HP-WFF ;
attrp is canonical  means :Def7: :: HILBERT3:def 7
 for V being SetValuation ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p);
end;

:: deftheorem Def7 defines canonical HILBERT3:def_7_:_
 for p being Element of HP-WFF holds
( p is canonical iff for V being SetValuation ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) );

registration
cluster VERUM  ->  canonical ;
coherence
 VERUM is canonical
proofend;
end;

registration
let p, q be Element of HP-WFF ;
clusterp => (q => p) ->  canonical ;
coherence
 p => (q => p) is canonical
proofend;
cluster(p '&amp;' q) => p ->  canonical ;
coherence
 (p '&amp;' q) => p is canonical
proofend;
cluster(p '&amp;' q) => q ->  canonical ;
coherence
 (p '&amp;' q) => q is canonical
proofend;
clusterp => (q => (p '&amp;' q)) ->  canonical ;
coherence
 p => (q => (p '&amp;' q)) is canonical
proofend;
end;

registration
let p, q, r be Element of HP-WFF ;
cluster(p => (q => r)) => ((p => q) => (p => r)) ->  canonical ;
coherence
 (p => (q => r)) => ((p => q) => (p => r)) is canonical
proofend;
end;

theorem Th41: :: HILBERT3:41
for p, q being Element of HP-WFF st p is canonical &amp; p => q is canonical holds
q is canonical
proofend;

theorem :: HILBERT3:42
for p being Element of HP-WFF st p in HP_TAUT holds
p is canonical
proofend;

registration
cluster Relation-like Function-like V51() canonical for Element of HP-WFF ;
existence
 ex b1 being Element of HP-WFF st b1 is canonical
proofend;
end;

begin

definition
let p be Element of HP-WFF ;
attrp is pseudo-canonical  means :Def8: :: HILBERT3:def 8
 for V being SetValuation
for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p);
end;

:: deftheorem Def8 defines pseudo-canonical HILBERT3:def_8_:_
 for p being Element of HP-WFF holds
( p is pseudo-canonical iff for V being SetValuation
for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p) );

registration
cluster canonical  ->  pseudo-canonical for Element of HP-WFF ;
coherence
 for b1 being Element of HP-WFF st b1 is canonical holds
b1 is pseudo-canonical
proofend;
end;

theorem :: HILBERT3:43
for p, q being Element of HP-WFF st p is pseudo-canonical &amp; p => q is pseudo-canonical holds
q is pseudo-canonical
proofend;

theorem Th44: :: HILBERT3:44
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm (P,p) &amp; ( for f being set holds not f is_a_fixpoint_of Perm (P,q) ) holds
not p => q is pseudo-canonical
proofend;

theorem :: HILBERT3:45
for a, b being Element of NAT st a <> b holds
not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical
proofend;