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 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
dprdff.1 ( 𝜑𝐺 dom DProd 𝑆 )
dprdff.2 ( 𝜑 → dom 𝑆 = 𝐼 )
dprdff.3 ( 𝜑𝐹𝑊 )
dprdfcntz.z 𝑍 = ( Cntz ‘ 𝐺 )
Assertion dprdfcntz ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dprdff.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
2 dprdff.1 ( 𝜑𝐺 dom DProd 𝑆 )
3 dprdff.2 ( 𝜑 → dom 𝑆 = 𝐼 )
4 dprdff.3 ( 𝜑𝐹𝑊 )
5 dprdfcntz.z 𝑍 = ( Cntz ‘ 𝐺 )
6 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 1 2 3 4 6 dprdff ( 𝜑𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
8 7 ffnd ( 𝜑𝐹 Fn 𝐼 )
9 7 ffvelrnda ( ( 𝜑𝑦𝐼 ) → ( 𝐹𝑦 ) ∈ ( Base ‘ 𝐺 ) )
10 simpr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
11 10 fveq2d ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦 = 𝑧 ) → ( 𝐹𝑦 ) = ( 𝐹𝑧 ) )
12 10 equcomd ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦 = 𝑧 ) → 𝑧 = 𝑦 )
13 12 fveq2d ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦 = 𝑧 ) → ( 𝐹𝑧 ) = ( 𝐹𝑦 ) )
14 11 13 oveq12d ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦 = 𝑧 ) → ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) )
15 2 ad3antrrr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → 𝐺 dom DProd 𝑆 )
16 3 ad3antrrr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → dom 𝑆 = 𝐼 )
17 simpllr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → 𝑦𝐼 )
18 simplr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → 𝑧𝐼 )
19 simpr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → 𝑦𝑧 )
20 15 16 17 18 19 5 dprdcntz ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → ( 𝑆𝑦 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑧 ) ) )
21 1 2 3 4 dprdfcl ( ( 𝜑𝑦𝐼 ) → ( 𝐹𝑦 ) ∈ ( 𝑆𝑦 ) )
22 21 ad2antrr ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → ( 𝐹𝑦 ) ∈ ( 𝑆𝑦 ) )
23 20 22 sseldd ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ( 𝑆𝑧 ) ) )
24 1 2 3 4 dprdfcl ( ( 𝜑𝑧𝐼 ) → ( 𝐹𝑧 ) ∈ ( 𝑆𝑧 ) )
25 24 ad4ant13 ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → ( 𝐹𝑧 ) ∈ ( 𝑆𝑧 ) )
26 eqid ( +g𝐺 ) = ( +g𝐺 )
27 26 5 cntzi ( ( ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ( 𝑆𝑧 ) ) ∧ ( 𝐹𝑧 ) ∈ ( 𝑆𝑧 ) ) → ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) )
28 23 25 27 syl2anc ( ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) ∧ 𝑦𝑧 ) → ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) )
29 14 28 pm2.61dane ( ( ( 𝜑𝑦𝐼 ) ∧ 𝑧𝐼 ) → ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) )
30 29 ralrimiva ( ( 𝜑𝑦𝐼 ) → ∀ 𝑧𝐼 ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) )
31 8 adantr ( ( 𝜑𝑦𝐼 ) → 𝐹 Fn 𝐼 )
32 oveq2 ( 𝑥 = ( 𝐹𝑧 ) → ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) )
33 oveq1 ( 𝑥 = ( 𝐹𝑧 ) → ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) )
34 32 33 eqeq12d ( 𝑥 = ( 𝐹𝑧 ) → ( ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) ↔ ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) ) )
35 34 ralrn ( 𝐹 Fn 𝐼 → ( ∀ 𝑥 ∈ ran 𝐹 ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) ↔ ∀ 𝑧𝐼 ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) ) )
36 31 35 syl ( ( 𝜑𝑦𝐼 ) → ( ∀ 𝑥 ∈ ran 𝐹 ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) ↔ ∀ 𝑧𝐼 ( ( 𝐹𝑦 ) ( +g𝐺 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑧 ) ( +g𝐺 ) ( 𝐹𝑦 ) ) ) )
37 30 36 mpbird ( ( 𝜑𝑦𝐼 ) → ∀ 𝑥 ∈ ran 𝐹 ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) )
38 7 frnd ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
39 38 adantr ( ( 𝜑𝑦𝐼 ) → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
40 6 26 5 elcntz ( ran 𝐹 ⊆ ( Base ‘ 𝐺 ) → ( ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ran 𝐹 ) ↔ ( ( 𝐹𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) ) ) )
41 39 40 syl ( ( 𝜑𝑦𝐼 ) → ( ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ran 𝐹 ) ↔ ( ( 𝐹𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ( ( 𝐹𝑦 ) ( +g𝐺 ) 𝑥 ) = ( 𝑥 ( +g𝐺 ) ( 𝐹𝑦 ) ) ) ) )
42 9 37 41 mpbir2and ( ( 𝜑𝑦𝐼 ) → ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ran 𝐹 ) )
43 42 ralrimiva ( 𝜑 → ∀ 𝑦𝐼 ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ran 𝐹 ) )
44 ffnfv ( 𝐹 : 𝐼 ⟶ ( 𝑍 ‘ ran 𝐹 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑦𝐼 ( 𝐹𝑦 ) ∈ ( 𝑍 ‘ ran 𝐹 ) ) )
45 8 43 44 sylanbrc ( 𝜑𝐹 : 𝐼 ⟶ ( 𝑍 ‘ ran 𝐹 ) )
46 45 frnd ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )