Step |
Hyp |
Ref |
Expression |
1 |
|
dprdff.w |
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. } |
2 |
|
dprdff.1 |
|- ( ph -> G dom DProd S ) |
3 |
|
dprdff.2 |
|- ( ph -> dom S = I ) |
4 |
|
dprdff.3 |
|- ( ph -> F e. W ) |
5 |
|
dprdfcntz.z |
|- Z = ( Cntz ` G ) |
6 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
7 |
1 2 3 4 6
|
dprdff |
|- ( ph -> F : I --> ( Base ` G ) ) |
8 |
7
|
ffnd |
|- ( ph -> F Fn I ) |
9 |
7
|
ffvelrnda |
|- ( ( ph /\ y e. I ) -> ( F ` y ) e. ( Base ` G ) ) |
10 |
|
simpr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y = z ) -> y = z ) |
11 |
10
|
fveq2d |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y = z ) -> ( F ` y ) = ( F ` z ) ) |
12 |
10
|
equcomd |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y = z ) -> z = y ) |
13 |
12
|
fveq2d |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y = z ) -> ( F ` z ) = ( F ` y ) ) |
14 |
11 13
|
oveq12d |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y = z ) -> ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) |
15 |
2
|
ad3antrrr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> G dom DProd S ) |
16 |
3
|
ad3antrrr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> dom S = I ) |
17 |
|
simpllr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> y e. I ) |
18 |
|
simplr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> z e. I ) |
19 |
|
simpr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> y =/= z ) |
20 |
15 16 17 18 19 5
|
dprdcntz |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> ( S ` y ) C_ ( Z ` ( S ` z ) ) ) |
21 |
1 2 3 4
|
dprdfcl |
|- ( ( ph /\ y e. I ) -> ( F ` y ) e. ( S ` y ) ) |
22 |
21
|
ad2antrr |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> ( F ` y ) e. ( S ` y ) ) |
23 |
20 22
|
sseldd |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> ( F ` y ) e. ( Z ` ( S ` z ) ) ) |
24 |
1 2 3 4
|
dprdfcl |
|- ( ( ph /\ z e. I ) -> ( F ` z ) e. ( S ` z ) ) |
25 |
24
|
ad4ant13 |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> ( F ` z ) e. ( S ` z ) ) |
26 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
27 |
26 5
|
cntzi |
|- ( ( ( F ` y ) e. ( Z ` ( S ` z ) ) /\ ( F ` z ) e. ( S ` z ) ) -> ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) |
28 |
23 25 27
|
syl2anc |
|- ( ( ( ( ph /\ y e. I ) /\ z e. I ) /\ y =/= z ) -> ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) |
29 |
14 28
|
pm2.61dane |
|- ( ( ( ph /\ y e. I ) /\ z e. I ) -> ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) |
30 |
29
|
ralrimiva |
|- ( ( ph /\ y e. I ) -> A. z e. I ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) |
31 |
8
|
adantr |
|- ( ( ph /\ y e. I ) -> F Fn I ) |
32 |
|
oveq2 |
|- ( x = ( F ` z ) -> ( ( F ` y ) ( +g ` G ) x ) = ( ( F ` y ) ( +g ` G ) ( F ` z ) ) ) |
33 |
|
oveq1 |
|- ( x = ( F ` z ) -> ( x ( +g ` G ) ( F ` y ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) |
34 |
32 33
|
eqeq12d |
|- ( x = ( F ` z ) -> ( ( ( F ` y ) ( +g ` G ) x ) = ( x ( +g ` G ) ( F ` y ) ) <-> ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) ) |
35 |
34
|
ralrn |
|- ( F Fn I -> ( A. x e. ran F ( ( F ` y ) ( +g ` G ) x ) = ( x ( +g ` G ) ( F ` y ) ) <-> A. z e. I ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) ) |
36 |
31 35
|
syl |
|- ( ( ph /\ y e. I ) -> ( A. x e. ran F ( ( F ` y ) ( +g ` G ) x ) = ( x ( +g ` G ) ( F ` y ) ) <-> A. z e. I ( ( F ` y ) ( +g ` G ) ( F ` z ) ) = ( ( F ` z ) ( +g ` G ) ( F ` y ) ) ) ) |
37 |
30 36
|
mpbird |
|- ( ( ph /\ y e. I ) -> A. x e. ran F ( ( F ` y ) ( +g ` G ) x ) = ( x ( +g ` G ) ( F ` y ) ) ) |
38 |
7
|
frnd |
|- ( ph -> ran F C_ ( Base ` G ) ) |
39 |
38
|
adantr |
|- ( ( ph /\ y e. I ) -> ran F C_ ( Base ` G ) ) |
40 |
6 26 5
|
elcntz |
|- ( ran F C_ ( Base ` G ) -> ( ( F ` y ) e. ( Z ` ran F ) <-> ( ( F ` y ) e. ( Base ` G ) /\ A. x e. ran F ( ( F ` y ) ( +g ` G ) x ) = ( x ( +g ` G ) ( F ` y ) ) ) ) ) |
41 |
39 40
|
syl |
|- ( ( ph /\ y e. I ) -> ( ( F ` y ) e. ( Z ` ran F ) <-> ( ( F ` y ) e. ( Base ` G ) /\ A. x e. ran F ( ( F ` y ) ( +g ` G ) x ) = ( x ( +g ` G ) ( F ` y ) ) ) ) ) |
42 |
9 37 41
|
mpbir2and |
|- ( ( ph /\ y e. I ) -> ( F ` y ) e. ( Z ` ran F ) ) |
43 |
42
|
ralrimiva |
|- ( ph -> A. y e. I ( F ` y ) e. ( Z ` ran F ) ) |
44 |
|
ffnfv |
|- ( F : I --> ( Z ` ran F ) <-> ( F Fn I /\ A. y e. I ( F ` y ) e. ( Z ` ran F ) ) ) |
45 |
8 43 44
|
sylanbrc |
|- ( ph -> F : I --> ( Z ` ran F ) ) |
46 |
45
|
frnd |
|- ( ph -> ran F C_ ( Z ` ran F ) ) |