let G be Group; for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
let I be non empty set ; for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
let F be componentwise_strict Subgroup-Family of I,G; for Fam being Subset of (Subgroups G) st Fam = rng F holds
for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
let Fam be Subset of (Subgroups G); ( Fam = rng F implies for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J)) )
assume A1:
Fam = rng F
; for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
let H be strict Subgroup of G; for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
let i be Element of I; ( H = F . i implies for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J)) )
assume A3:
H = F . i
; for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
let J be Subset of I; ( J = I \ { j where j is Element of I : F . i = F . j } implies union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J)) )
assume A4:
J = I \ { j where j is Element of I : F . i = F . j }
; union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
set X = { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } ;
for x being object holds
( x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } iff x in rng (Carrier (F | J)) )
proof
let x be
object ;
( x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } iff x in rng (Carrier (F | J)) )
thus
(
x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } implies
x in rng (Carrier (F | J)) )
( x in rng (Carrier (F | J)) implies x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } )proof
assume
x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) }
;
x in rng (Carrier (F | J))
then consider A being
Subset of
G such that B2:
(
A = x & ex
K being
strict Subgroup of
G st
(
K in Fam &
A = the
carrier of
K &
K <> H ) )
;
consider K being
strict Subgroup of
G such that B3:
(
K in Fam &
A = the
carrier of
K &
K <> H )
by B2;
consider j being
Element of
I such that B4:
F . j = K
by A1, B3, MssRng;
B5:
(
dom (F | J) = J &
dom (Carrier (F | J)) = J )
by PARTFUN1:def 2;
B6:
j in J
then reconsider j =
j as
Element of
J ;
reconsider Fj =
(F | J) . j as
Subgroup of
G by B6, GROUP_20:def 1;
B7:
(Carrier (F | J)) . j = the
carrier of
Fj
by B6, Th9;
A = (Carrier (F | J)) . j
by B3, B4, B6, B7, FUNCT_1:49;
hence
x in rng (Carrier (F | J))
by B2, B5, B6, FUNCT_1:3;
verum
end;
assume
x in rng (Carrier (F | J))
;
x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) }
then consider j0 being
object such that Z3:
(
j0 in dom (Carrier (F | J)) &
x = (Carrier (F | J)) . j0 )
by FUNCT_1:def 3;
reconsider j =
j0 as
Element of
J by Z3;
Z5:
j in J
by Z3;
reconsider Fj =
(F | J) . j as
Subgroup of
G by Z3, GROUP_20:def 1;
reconsider A = the
carrier of
Fj as
Subset of
G by GROUP_2:def 5;
Z5b:
Fj = F . j
by Z3, FUNCT_1:49;
Z6:
Fj in Fam
Z7:
Fj <> H
Z8:
x = the
carrier of
Fj
by Z3, Th9;
ex
K being
strict Subgroup of
G st
(
K in Fam &
A = the
carrier of
K &
K <> H )
hence
x in { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) }
by Z8;
verum
end;
then
{ A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = rng (Carrier (F | J))
by TARSKI:2;
hence
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))
by CARD_3:def 4; verum