let p, q, r be Element of HP-WFF ; :: thesis: (p => (q => r)) => ((p => q) => (p => r)) is canonical
let V be SetValuation; :: according to HILBERT3:def 7 :: thesis: ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm P,((p => (q => r)) => ((p => q) => (p => r)))
A1:
( SetVal V,(p => q) = Funcs (SetVal V,p),(SetVal V,q) & SetVal V,(p => r) = Funcs (SetVal V,p),(SetVal V,r) )
by Def2;
deffunc H1( Function) -> set = Frege $1;
A2:
for x being Element of SetVal V,(p => (q => r)) holds H1(x) in SetVal V,((p => q) => (p => r))
proof
let x be
Element of
SetVal V,
(p => (q => r));
:: thesis: H1(x) in SetVal V,((p => q) => (p => r))
x is
Element of
Funcs (SetVal V,p),
(SetVal V,(q => r))
by Def2;
then
x is
Element of
Funcs (SetVal V,p),
(Funcs (SetVal V,q),(SetVal V,r))
by Def2;
then
Frege x is
Function of
(SetVal V,(p => q)),
(SetVal V,(p => r))
by A1, Th24;
then
Frege x in Funcs (SetVal V,(p => q)),
(SetVal V,(p => r))
by FUNCT_2:11;
hence
Frege x in SetVal V,
((p => q) => (p => r))
by Def2;
:: thesis: verum
end;
consider F being Function of (SetVal V,(p => (q => r))),(SetVal V,((p => q) => (p => r))) such that
A3:
for x being Element of SetVal V,(p => (q => r)) holds F . x = H1(x)
from FUNCT_2:sch 8(A2);
take
F
; :: thesis: for P being Permutation of V holds F is_a_fixpoint_of Perm P,((p => (q => r)) => ((p => q) => (p => r)))
let P be Permutation of V; :: thesis: F is_a_fixpoint_of Perm P,((p => (q => r)) => ((p => q) => (p => r)))
F in Funcs (SetVal V,(p => (q => r))),(SetVal V,((p => q) => (p => r)))
by FUNCT_2:11;
then
F in SetVal V,((p => (q => r)) => ((p => q) => (p => r)))
by Def2;
hence
F in dom (Perm P,((p => (q => r)) => ((p => q) => (p => r))))
by FUNCT_2:def 1; :: according to ABIAN:def 3 :: thesis: F = (Perm P,((p => (q => r)) => ((p => q) => (p => r)))) . F
now let f be
Element of
SetVal V,
(p => (q => r));
:: thesis: F . f = (((Perm P,((p => q) => (p => r))) * F) * ((Perm P,(p => (q => r))) " )) . freconsider X =
(Perm P,(q => r)) " as
Function of
(SetVal V,(q => r)),
(SetVal V,(q => r)) ;
f in SetVal V,
(p => (q => r))
;
then
f in Funcs (SetVal V,p),
(SetVal V,(q => r))
by Def2;
then reconsider ff =
f as
Function of
(SetVal V,p),
(SetVal V,(q => r)) by FUNCT_2:121;
A4:
SetVal V,
(q => r) = Funcs (SetVal V,q),
(SetVal V,r)
by Def2;
then A5:
product (doms ff) =
product ((SetVal V,p) --> (SetVal V,q))
by Th6
.=
Funcs (SetVal V,p),
(SetVal V,q)
by CARD_3:20
;
then A6:
product (doms ff) = SetVal V,
(p => q)
by Def2;
set Yf =
((Perm P,(p => (q => r))) " ) . f;
((Perm P,(p => (q => r))) " ) . f = (((Perm P,(q => r)) " ) * ff) * (Perm P,p)
by Th38;
then reconsider h =
Frege (((Perm P,(p => (q => r))) " ) . f) as
Function-yielding Function of
(SetVal V,(p => q)),
(SetVal V,(p => r)) by A1, A4, Th24;
set M =
((Perm P,(p => r)) * h) * ((Perm P,(p => q)) " );
reconsider M =
((Perm P,(p => r)) * h) * ((Perm P,(p => q)) " ) as
ManySortedFunction of
by A6;
A7:
for
g being
Function st
g in product (doms f) holds
M . g = f .. g
proof
let g be
Function;
:: thesis: ( g in product (doms f) implies M . g = f .. g )
assume A8:
g in product (doms f)
;
:: thesis: M . g = f .. g
reconsider G =
g as
Function of
(SetVal V,p),
(SetVal V,q) by A5, A8, FUNCT_2:121;
reconsider FF =
ff as
Function of
(SetVal V,p),
(Funcs (SetVal V,q),(SetVal V,r)) by Def2;
dom FF = SetVal V,
p
by FUNCT_2:def 1;
then A9:
dom (FF .. G) = SetVal V,
p
by PRALG_1:def 17;
A10:
rng (FF .. G) c= SetVal V,
r
by Th20;
then
FF .. G is
Function of
(SetVal V,p),
(SetVal V,r)
by A9, FUNCT_2:def 1, RELSET_1:11;
then
FF .. G in Funcs (SetVal V,p),
(SetVal V,r)
by FUNCT_2:11;
then A11:
FF .. G in SetVal V,
(p => r)
by Def2;
reconsider GG =
FF .. G as
Function of
(SetVal V,p),
(SetVal V,r) by A9, A10, FUNCT_2:def 1, RELSET_1:11;
((Perm P,(p => (q => r))) " ) . f in SetVal V,
(p => (q => r))
;
then
((Perm P,(p => (q => r))) " ) . f in Funcs (SetVal V,p),
(SetVal V,(q => r))
by Def2;
then
((Perm P,(p => (q => r))) " ) . f is
Function of
(SetVal V,p),
(Funcs (SetVal V,q),(SetVal V,r))
by A4, FUNCT_2:121;
then A12:
product (doms (((Perm P,(p => (q => r))) " ) . f)) =
product ((SetVal V,p) --> (SetVal V,q))
by Th6
.=
Funcs (SetVal V,p),
(SetVal V,q)
by CARD_3:20
.=
SetVal V,
(p => q)
by Def2
;
(((Perm P,q) " ) * G) * (Perm P,p) in Funcs (SetVal V,p),
(SetVal V,q)
by FUNCT_2:11;
then A13:
(((Perm P,q) " ) * g) * (Perm P,p) in product (doms (((Perm P,(p => (q => r))) " ) . f))
by A12, Def2;
then A14:
((Perm P,(p => q)) " ) . G in SetVal V,
(p => q)
by A12, Th38;
A15:
X =
((Perm P,q) => (Perm P,r)) "
by Th36
.=
((Perm P,q) " ) => ((Perm P,r) " )
by Th27
;
A16:
h . (((Perm P,(p => q)) " ) . g) =
h . ((((Perm P,q) " ) * G) * (Perm P,p))
by Th38
.=
(((Perm P,(p => (q => r))) " ) . f) .. ((((Perm P,q) " ) * g) * (Perm P,p))
by A13, PRALG_2:def 8
.=
((X * ff) * (Perm P,p)) .. ((((Perm P,q) " ) * g) * (Perm P,p))
by Th38
.=
((X * FF) .. (((Perm P,q) " ) * g)) * (Perm P,p)
by Th18
.=
(((Perm P,r) " ) * (FF .. G)) * (Perm P,p)
by A15, Th28
.=
((Perm P,(p => r)) " ) . GG
by Th38
;
thus M . g =
((Perm P,(p => r)) * h) . (((Perm P,(p => q)) " ) . g)
by A6, A8, FUNCT_2:21
.=
(Perm P,(p => r)) . (((Perm P,(p => r)) " ) . GG)
by A14, A16, FUNCT_2:21
.=
((Perm P,(p => r)) * ((Perm P,(p => r)) " )) . GG
by A11, FUNCT_2:21
.=
(id (SetVal V,(p => r))) . GG
by FUNCT_2:88
.=
f .. g
by A11, FUNCT_1:35
;
:: thesis: verum
end; thus F . f =
Frege f
by A3
.=
((Perm P,(p => r)) * h) * ((Perm P,(p => q)) " )
by A7, PRALG_2:def 8
.=
(Perm P,((p => q) => (p => r))) . h
by Th37
.=
(Perm P,((p => q) => (p => r))) . (F . (((Perm P,(p => (q => r))) " ) . f))
by A3
.=
((Perm P,((p => q) => (p => r))) * F) . (((Perm P,(p => (q => r))) " ) . f)
by FUNCT_2:21
.=
(((Perm P,((p => q) => (p => r))) * F) * ((Perm P,(p => (q => r))) " )) . f
by FUNCT_2:21
;
:: thesis: verum end;
hence F =
((Perm P,((p => q) => (p => r))) * F) * ((Perm P,(p => (q => r))) " )
by FUNCT_2:113
.=
(Perm P,((p => (q => r)) => ((p => q) => (p => r)))) . F
by Th37
;
:: thesis: verum