Re: Mizar theorem GROUP_6:93

Dear Alex:
Thank you for the explanation.
Victor

On Fri, Dec 8, 2023 at 9:47=E2=80=AFAM Alex Nelson thmprover _AT_ gmail.com
<[email protected]> wrote:
>
> Hello,
>
> So here's my understanding: suppose we have in Mizar a "N being normal Su=
bgroup of G" and "H being Subgroup of G". We know that if `N` is a Subgroup=
 of `H`, then `N` is a normal subgroup of H. However, Mizar does not know t=
his. To communicate this to Mizar, we introduce this "hack", writing "(H,N)=
`*`" to say "Consider N as a normal Subgroup of H".
>
> This allows us to do things like write down "H./.(H,N)`*`" whereas in Mat=
hematics we could write down H/N.
>
> Similarly, the group SN in Mizar is S "\/" N. Mathematics is actually qui=
te sloppy in its notation here, since SN should not be confused with the se=
t S*N. The group S "\/" N is defined in GROUP_4 as the lattice join of subg=
roups, i.e., the subgroup generated by S*N, or in Mizar code "gr ((carr S)*=
(carr N))". (See https://mizar.uwb.edu.pl/version/current/html/group_4.html=
#K8)
>
> Now, we see the two groups which are declared isomorphic are (B "\/" N)./=
.(B "\/" N,N)`*` --- which in "normal mathematics" is BN/N --- and B./.(B /=
\ N) --- which is "normal mathematics" is B/(B\cap N).
>
> I hope this helps, I just woke up and have yet to have my morning coffee,=
 so I might have erred accidentally in my excitement to answer.
>
> Best,
> Alex
>
> On Fri, Dec 8, 2023 at 5:56=E2=80=AFAM Victor Makarov viktmak _AT_ gmail.=
com <[email protected]> wrote:
>>
>> Dear Forum:
>>
>> I am trying to understand the statement of the theorem GROUP_6:93:
>>
>> https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVk/NDA9PyNzODcrNSNsYTg1N=
D81NCN2bGJrZHFwd2A4PWM1MzJjZDRjNmBmNzQ0ZmA9NmRkNzM0M2RkPWBjYDFmYGE3ZmcxNCNx=
ODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHc=
oY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=3Dhttp%3a%2f%2fmizar.org%=
2fJFM%2fVol3%2fgroup_6.abs.html%23K2
>>
>> theorem :: GROUP_6:93
>>    for N being strict normal Subgroup of G holds
>>  (B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic;
>>
>> What does mean (B "\/" N)" and (B "\/" N,N)`*` ?
>>
>> How is the theorem  GROUP_6:93 related to the Second Isomorphism Theorem=
?
>>
>> Second Isomorphism Theorem:
>> (Theorem B in Wikipedia):
>> https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVk/NDA9PyNzODcrNSNsYTg1N=
D81NCN2bGJrZHFwd2A4MWEwYTYyMTZkMz02NzIzZDdmM2Y0ZmBkPDAxPGQ0N2AyNjI3NTIxMSNx=
ODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHc=
oY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=3Dhttps%3a%2f%2fen.wikipe=
dia.org%2fwiki%2fIsomorphism_theorems
>>
>> Theorem B (groups)
>>
>> Let G be a group. Let S be a subgroup of G, and let N be a normal subgro=
up of G.
>>  Then the following hold:
>>
>> The product SN is a subgroup of G,
>> The subgroup N is a normal subgroup of SN},
>> The intersection S/\N is a normal subgroup of S, and
>> The quotient groups (SN)/N and S/(S/\N)} are isomorphic.
>> (Wikipedia uses another symbol(\cap) for the intersection).
>>
>> Thanks in advance,
>>
>> Victor Makarov
>>