let I be non empty set ; for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )
let G be Group; for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )
let F be component-commutative Subgroup-Family of I,G; for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )
let UF be Subset of G; ( UF = Union (Carrier F) implies for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f ) )
assume A1:
UF = Union (Carrier F)
; for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )
defpred S1[ Nat] means for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = $1 & len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f );
A2:
S1[ 0 ]
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
S1[n + 1]
let g be
Element of
G;
for H being FinSequence of G
for K being FinSequence of INT st len H = n + 1 & len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )let H be
FinSequence of
G;
for K being FinSequence of INT st len H = n + 1 & len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )let K be
FinSequence of
INT ;
( len H = n + 1 & len H = len K & rng H c= UF & Product (H |^ K) = g implies ex f being finite-support Function of I,G st
( f in product F & g = Product f ) )
assume A7:
(
len H = n + 1 &
len H = len K &
rng H c= UF &
Product (H |^ K) = g )
;
ex f being finite-support Function of I,G st
( f in product F & g = Product f )
reconsider h =
H /. (n + 1) as
Element of
G ;
reconsider k =
K /. (n + 1) as
Element of
INT ;
reconsider H0 =
H | n as
FinSequence of
G ;
reconsider K0 =
K | n as
FinSequence of
INT ;
reconsider H1 =
<*h*> as
FinSequence of
G ;
reconsider K1 =
<*k*> as
FinSequence of
INT ;
rng H0 c= rng H
by RELAT_1:70;
then A8:
rng H0 c= UF
by A7;
A9:
<*(@ k)*> = K1
by GROUP_4:def 1;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then A10:
(
n + 1
in dom H &
n + 1
in dom K )
by A7, FINSEQ_1:def 3;
then
(
H /. (n + 1) = H . (n + 1) &
K /. (n + 1) = K . (n + 1) )
by PARTFUN1:def 6;
then A11:
(
H = H0 ^ H1 &
K = K0 ^ K1 )
by A7, FINSEQ_3:55;
h = H . (n + 1)
by A10, PARTFUN1:def 6;
then A12:
h in UF
by A7, A10, FUNCT_1:3;
(
n <= len H &
n <= len K )
by A7, XREAL_1:31;
then A13:
(
len H0 = n &
len K0 = n )
by FINSEQ_1:17;
A14:
(
len H1 = 1 &
len K1 = 1 )
by FINSEQ_1:39;
A15:
H |^ K =
(H0 |^ K0) ^ (H1 |^ K1)
by A11, A13, A14, GROUP_4:19
.=
(H0 |^ K0) ^ <*(h |^ k)*>
by A9, GROUP_4:22
;
consider f0 being
finite-support Function of
I,
G such that A16:
(
f0 in product F &
Product (H0 |^ K0) = Product f0 )
by A6, A8, A13;
h in union (rng (Carrier F))
by A1, A12, CARD_3:def 4;
then consider Fi being
set such that A17:
(
h in Fi &
Fi in rng (Carrier F) )
by TARSKI:def 4;
consider i being
object such that A18:
(
i in dom (Carrier F) &
Fi = (Carrier F) . i )
by A17, FUNCT_1:def 3;
reconsider i =
i as
Element of
I by A18;
A19:
F . i is
Subgroup of
G
by Def1;
(Carrier F) . i = [#] (F . i)
by PENCIL_3:7;
then
h in F . i
by A17, A18;
then A22:
h |^ k in F . i
by A19, GROUP_4:4;
A23:
f0 . i in F . i
by A16, GROUP_19:5;
1_ (F . i) is
Element of
G
by A19, GROUP_2:42;
then reconsider f1 =
f0 +* (
i,
(1_ (F . i))) as
finite-support Function of
I,
G by GROUP_19:26;
reconsider f =
f1 +* (
i,
((f0 . i) * (h |^ k))) as
finite-support Function of
I,
G by GROUP_19:26;
A27:
dom f0 = I
by FUNCT_2:def 1;
A28:
dom f1 = I
by FUNCT_2:def 1;
A29:
f1 in product F
by A16, GROUP_19:24;
A30:
f . i = (f0 . i) * (h |^ k)
by A28, FUNCT_7:31;
take
f
;
( f in product F & g = Product f )
(f0 . i) * (h |^ k) in F . i
by A19, A22, A23, GROUP_2:50;
hence A31:
f in product F
by A29, GROUP_19:24;
g = Product f
f1 . i = 1_ (F . i)
by A27, FUNCT_7:31;
then
f1 = f +* (
i,
(1_ (F . i)))
by Th7;
then Product f =
(Product f1) * ((f0 . i) * (h |^ k))
by A30, A31, Th8
.=
((Product f1) * (f0 . i)) * (h |^ k)
by GROUP_1:def 3
.=
(Product f0) * (h |^ k)
by A16, Th8
.=
g
by A7, A15, A16, GROUP_4:6
;
hence
g = Product f
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A5);
hence
for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )
; verum