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 \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
	dprdff.1	$⊢ φ \to G dom DProd S$
	dprdff.2	$⊢ φ \to dom S = I$
	dprdff.3	$⊢ φ \to F \in W$
	dprdfcntz.z	$⊢ Z = Cntz (G)$
Assertion	dprdfcntz	$⊢ φ \to ran F \subseteq Z (ran F)$

Proof

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

Metamath Proof Explorer

Theorem dprdfcntz

Proof