This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 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 𝐹 ) )