Metamath Proof Explorer

Theorem dprdfcntz

Description: A function on the elements of an internal direct product has pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Hypotheses dprdff.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
dprdff.1 
|- ( ph -> G dom DProd S )
dprdff.2 
|- ( ph -> dom S = I )
dprdff.3 
|- ( ph -> F e. W )
dprdfcntz.z 
|- Z = ( Cntz ` G )
Assertion dprdfcntz 
|- ( ph -> ran F C_ ( Z ` ran F ) )

Proof

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 ) )