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

Metamath Proof Explorer

Theorem dprdfcntz

Proof