Re: Union of two subgroups

Received, thank you.

On Sat, Nov 21, 2020 at 12:51 PM Coghetto Roland <
[email protected]> wrote:

> Dear Victor,
>
> For the second question: " about the product of two subgroups H and K:
> H*K is a subgroup iff H*K = K*H.", with Adam's suggestion
>
> Roland
>
> ========
> environ
>
>  vocabularies GROUP_1, STRUCT_0, GROUP_2,SUBSET_1, RELAT_1, TARSKI,EQREL_1,
>    GROUP_4;
>  notations TARSKI, STRUCT_0, ALGSTR_0, GROUP_2, GROUP_1, GROUP_4;
>  constructors NAT_1, FINSOP_1, GROUP_4;
>  registrations STRUCT_0, GROUP_2;
>  requirements BOOLE, SUBSET;
>  equalities GROUP_2, GROUP_4;
>  expansions TARSKI, XBOOLE_0;
>  theorems GROUP_1, GROUP_2,GROUP_4;
>
> begin
>
> theorem
>   for G being Group for H,K being Subgroup of G holds
>   (ex HK being Subgroup of G st the carrier of HK = H * K) iff
>   H * K = K * H
>   proof
>     let G be Group;
>     let H,K be Subgroup of G;
>     now
>       hereby
>         assume H * K = K * H;
>         then
> A1:     the carrier of (H "\/" K) = H * K & H "\/" K = gr(H * K)
>           by GROUP_4:50,51;
>         reconsider HK = gr(H * K) as Subgroup of G;
>         take HK;
>         thus the carrier of HK = H * K by A1;
>       end;
>       assume ex HK be Subgroup of G st the carrier of HK = H * K;
>       then consider HK be Subgroup of G such that
> A2:   the carrier of HK = H * K;
>       now
>         hereby
>           let x be object;
>           assume x in H * K;
>           then reconsider x9 = x as Element of HK by A2;
>           x9" in { h * k where h,k is Element of G : h in carr H &
>                                                      k in carr K} by A2;
>           then consider h1,k1 be Element of G such that
> A3:       x9" = h1 * k1 and
> A4:       h1 in carr H and
> A5:       k1 in carr K;
> A6:       x9 = (x9") "
>             .= (h1 * k1) " by A3,GROUP_2:48
>             .= k1" * h1" by GROUP_1:17;
>           reconsider k2 = k1 as Element of K by A5;
>           reconsider h2 = h1 as Element of H by A4;
>           k2" = k1" & h2" = h1" by GROUP_2:48;
>           hence x in K * H by A6;
>         end;
>         hereby
>           let x be object;
>           assume
> A7:       x in K * H;
>           consider k,h be Element of G such that
> A8:       x = k * h and
> A9:       k in carr K and
> A10:      h in carr H by A7;
>           reconsider h9 = h as Element of H by A10;
>           reconsider h99 = h" as Element of G;
> A11:      h9" is Element of H;
>           reconsider k9 = k as Element of K by A9;
>           reconsider k99 = k" as Element of G;
>           k9" is Element of K;
>           then h99 is Element of H & k99 is Element of K by A11,GROUP_2:48;
>           then h99 * k99 in H * K;
>           then reconsider kh = (k * h)" as Element of HK by A2,GROUP_1:17;
>           kh" is Element of HK;
>           then (k * h)" " is Element of HK by GROUP_2:48;
>           hence x in H * K by A2,A8;
>         end;
>       end;
>       then H * K c= K * H & K * H c= H * K;
>       hence H * K = K * H;
>     end;
>     hence thesis;
>   end;
>
>
>