let Q be AIM multLoop; :: thesis: ( Q is satisfying_TT & Q is satisfying_TL & Q is satisfying_TR & Q is satisfying_LR & Q is satisfying_LL & Q is satisfying_RR )
thus Q is satisfying_TT :: thesis: ( Q is satisfying_TL & Q is satisfying_TR & Q is satisfying_LR & Q is satisfying_LL & Q is satisfying_RR )
proof
let u, x, y be Element of Q; :: according to AIMLOOP:def 7 :: thesis: T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x)
set f = T_MAP x;
set g = T_MAP y;
A3: ( T_MAP x in InnAut Q & T_MAP y in InnAut Q ) by Th56;
T_map ((T_map (u,x)),y) = T_map (((T_MAP x) . u),y) by TM1
.= (T_MAP y) . ((T_MAP x) . u) by TM1
.= ((T_MAP y) * (T_MAP x)) . u by FUNCT_2:15
.= ((T_MAP x) * (T_MAP y)) . u by A3, Def50
.= (T_MAP x) . ((T_MAP y) . u) by FUNCT_2:15
.= T_map (((T_MAP y) . u),x) by TM1
.= T_map ((T_map (u,y)),x) by TM1 ;
hence T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x) ; :: thesis: verum
end;
thus Q is satisfying_TL :: thesis: ( Q is satisfying_TR & Q is satisfying_LR & Q is satisfying_LL & Q is satisfying_RR )
proof
let u, x, y, z be Element of Q; :: according to AIMLOOP:def 8 :: thesis: T_map ((L_map (u,x,y)),z) = L_map ((T_map (u,z)),x,y)
set f = L_MAP (x,y);
set g = T_MAP z;
A6: ( L_MAP (x,y) in InnAut Q & T_MAP z in InnAut Q ) by Th56, Th57;
T_map ((L_map (u,x,y)),z) = T_map (((L_MAP (x,y)) . u),z) by LM1
.= (T_MAP z) . ((L_MAP (x,y)) . u) by TM1
.= ((T_MAP z) * (L_MAP (x,y))) . u by FUNCT_2:15
.= ((L_MAP (x,y)) * (T_MAP z)) . u by A6, Def50
.= (L_MAP (x,y)) . ((T_MAP z) . u) by FUNCT_2:15
.= L_map (((T_MAP z) . u),x,y) by LM1
.= L_map ((T_map (u,z)),x,y) by TM1 ;
hence T_map ((L_map (u,x,y)),z) = L_map ((T_map (u,z)),x,y) ; :: thesis: verum
end;
thus Q is satisfying_TR :: thesis: ( Q is satisfying_LR & Q is satisfying_LL & Q is satisfying_RR )
proof
let u, x, y, z be Element of Q; :: according to AIMLOOP:def 9 :: thesis: T_map ((R_map (u,x,y)),z) = R_map ((T_map (u,z)),x,y)
set f = R_MAP (x,y);
set g = T_MAP z;
A9: ( R_MAP (x,y) in InnAut Q & T_MAP z in InnAut Q ) by Th56, Th58;
T_map ((R_map (u,x,y)),z) = T_map (((R_MAP (x,y)) . u),z) by RM1
.= (T_MAP z) . ((R_MAP (x,y)) . u) by TM1
.= ((T_MAP z) * (R_MAP (x,y))) . u by FUNCT_2:15
.= ((R_MAP (x,y)) * (T_MAP z)) . u by A9, Def50
.= (R_MAP (x,y)) . ((T_MAP z) . u) by FUNCT_2:15
.= R_map (((T_MAP z) . u),x,y) by RM1
.= R_map ((T_map (u,z)),x,y) by TM1 ;
hence T_map ((R_map (u,x,y)),z) = R_map ((T_map (u,z)),x,y) ; :: thesis: verum
end;
thus Q is satisfying_LR :: thesis: ( Q is satisfying_LL & Q is satisfying_RR )
proof
let u, x, y, z, w be Element of Q; :: according to AIMLOOP:def 10 :: thesis: L_map ((R_map (u,x,y)),z,w) = R_map ((L_map (u,z,w)),x,y)
set f = R_MAP (x,y);
set g = L_MAP (z,w);
A12: ( R_MAP (x,y) in InnAut Q & L_MAP (z,w) in InnAut Q ) by Th58, Th57;
L_map ((R_map (u,x,y)),z,w) = L_map (((R_MAP (x,y)) . u),z,w) by RM1
.= (L_MAP (z,w)) . ((R_MAP (x,y)) . u) by LM1
.= ((L_MAP (z,w)) * (R_MAP (x,y))) . u by FUNCT_2:15
.= ((R_MAP (x,y)) * (L_MAP (z,w))) . u by A12, Def50
.= (R_MAP (x,y)) . ((L_MAP (z,w)) . u) by FUNCT_2:15
.= R_map (((L_MAP (z,w)) . u),x,y) by RM1
.= R_map ((L_map (u,z,w)),x,y) by LM1 ;
hence L_map ((R_map (u,x,y)),z,w) = R_map ((L_map (u,z,w)),x,y) ; :: thesis: verum
end;
thus Q is satisfying_LL :: thesis: Q is satisfying_RR
proof
let u, x, y, z, w be Element of Q; :: according to AIMLOOP:def 11 :: thesis: L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y)
set f = L_MAP (x,y);
set g = L_MAP (z,w);
A15: ( L_MAP (x,y) in InnAut Q & L_MAP (z,w) in InnAut Q ) by Th57;
L_map ((L_map (u,x,y)),z,w) = L_map (((L_MAP (x,y)) . u),z,w) by LM1
.= (L_MAP (z,w)) . ((L_MAP (x,y)) . u) by LM1
.= ((L_MAP (z,w)) * (L_MAP (x,y))) . u by FUNCT_2:15
.= ((L_MAP (x,y)) * (L_MAP (z,w))) . u by A15, Def50
.= (L_MAP (x,y)) . ((L_MAP (z,w)) . u) by FUNCT_2:15
.= L_map (((L_MAP (z,w)) . u),x,y) by LM1
.= L_map ((L_map (u,z,w)),x,y) by LM1 ;
hence L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y) ; :: thesis: verum
end;
let u, x, y, z, w be Element of Q; :: according to AIMLOOP:def 12 :: thesis: R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y)
set f = R_MAP (x,y);
set g = R_MAP (z,w);
A18: ( R_MAP (x,y) in InnAut Q & R_MAP (z,w) in InnAut Q ) by Th58;
R_map ((R_map (u,x,y)),z,w) = R_map (((R_MAP (x,y)) . u),z,w) by RM1
.= (R_MAP (z,w)) . ((R_MAP (x,y)) . u) by RM1
.= ((R_MAP (z,w)) * (R_MAP (x,y))) . u by FUNCT_2:15
.= ((R_MAP (x,y)) * (R_MAP (z,w))) . u by A18, Def50
.= (R_MAP (x,y)) . ((R_MAP (z,w)) . u) by FUNCT_2:15
.= R_map (((R_MAP (z,w)) . u),x,y) by RM1
.= R_map ((R_map (u,z,w)),x,y) by RM1 ;
hence R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y) ; :: thesis: verum