unitprodclb

Description: A finite product is a unit iff all factors are units. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	unitprodclb.1	$⊢ B = {Base}_{R}$
	unitprodclb.u	$⊢ U = Unit (R)$
	unitprodclb.m	$⊢ M = {mulGrp}_{R}$
	unitprodclb.r	$⊢ φ \to R \in CRing$
	unitprodclb.f	$⊢ φ \to F \in Word B$
Assertion	unitprodclb	$⊢ φ \to (\sum_{M} F \in U \leftrightarrow ran F \subseteq U)$

Proof

Step	Hyp	Ref	Expression
1		unitprodclb.1	$⊢ B = {Base}_{R}$
2		unitprodclb.u	$⊢ U = Unit (R)$
3		unitprodclb.m	$⊢ M = {mulGrp}_{R}$
4		unitprodclb.r	$⊢ φ \to R \in CRing$
5		unitprodclb.f	$⊢ φ \to F \in Word B$
6		oveq2	$⊢ g = \emptyset \to \sum_{M} g = \sum_{M} \emptyset$
7	6	eleq1d	$⊢ g = \emptyset \to (\sum_{M} g \in U \leftrightarrow \sum_{M} \emptyset \in U)$
8		rneq	$⊢ g = \emptyset \to ran g = ran \emptyset$
9	8	sseq1d	$⊢ g = \emptyset \to (ran g \subseteq U \leftrightarrow ran \emptyset \subseteq U)$
10	7 9	bibi12d	$⊢ g = \emptyset \to ((\sum_{M} g \in U \leftrightarrow ran g \subseteq U) \leftrightarrow (\sum_{M} \emptyset \in U \leftrightarrow ran \emptyset \subseteq U))$
11	10	imbi2d	$⊢ g = \emptyset \to ((R \in CRing \to (\sum_{M} g \in U \leftrightarrow ran g \subseteq U)) \leftrightarrow (R \in CRing \to (\sum_{M} \emptyset \in U \leftrightarrow ran \emptyset \subseteq U)))$
12		oveq2	$⊢ g = f \to \sum_{M} g = \sum_{M} f$
13	12	eleq1d	$⊢ g = f \to (\sum_{M} g \in U \leftrightarrow \sum_{M} f \in U)$
14		rneq	$⊢ g = f \to ran g = ran f$
15	14	sseq1d	$⊢ g = f \to (ran g \subseteq U \leftrightarrow ran f \subseteq U)$
16	13 15	bibi12d	$⊢ g = f \to ((\sum_{M} g \in U \leftrightarrow ran g \subseteq U) \leftrightarrow (\sum_{M} f \in U \leftrightarrow ran f \subseteq U))$
17	16	imbi2d	$⊢ g = f \to ((R \in CRing \to (\sum_{M} g \in U \leftrightarrow ran g \subseteq U)) \leftrightarrow (R \in CRing \to (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)))$
18		oveq2	$⊢ g = f ++ ⟨“ x ”⟩ \to \sum_{M} g = \sum_{M} (f ++ ⟨“ x ”⟩)$
19	18	eleq1d	$⊢ g = f ++ ⟨“ x ”⟩ \to (\sum_{M} g \in U \leftrightarrow \sum_{M} (f ++ ⟨“ x ”⟩) \in U)$
20		rneq	$⊢ g = f ++ ⟨“ x ”⟩ \to ran g = ran (f ++ ⟨“ x ”⟩)$
21	20	sseq1d	$⊢ g = f ++ ⟨“ x ”⟩ \to (ran g \subseteq U \leftrightarrow ran (f ++ ⟨“ x ”⟩) \subseteq U)$
22	19 21	bibi12d	$⊢ g = f ++ ⟨“ x ”⟩ \to ((\sum_{M} g \in U \leftrightarrow ran g \subseteq U) \leftrightarrow (\sum_{M} (f ++ ⟨“ x ”⟩) \in U \leftrightarrow ran (f ++ ⟨“ x ”⟩) \subseteq U))$
23	22	imbi2d	$⊢ g = f ++ ⟨“ x ”⟩ \to ((R \in CRing \to (\sum_{M} g \in U \leftrightarrow ran g \subseteq U)) \leftrightarrow (R \in CRing \to (\sum_{M} (f ++ ⟨“ x ”⟩) \in U \leftrightarrow ran (f ++ ⟨“ x ”⟩) \subseteq U)))$
24		oveq2	$⊢ g = F \to \sum_{M} g = \sum_{M} F$
25	24	eleq1d	$⊢ g = F \to (\sum_{M} g \in U \leftrightarrow \sum_{M} F \in U)$
26		rneq	$⊢ g = F \to ran g = ran F$
27	26	sseq1d	$⊢ g = F \to (ran g \subseteq U \leftrightarrow ran F \subseteq U)$
28	25 27	bibi12d	$⊢ g = F \to ((\sum_{M} g \in U \leftrightarrow ran g \subseteq U) \leftrightarrow (\sum_{M} F \in U \leftrightarrow ran F \subseteq U))$
29	28	imbi2d	$⊢ g = F \to ((R \in CRing \to (\sum_{M} g \in U \leftrightarrow ran g \subseteq U)) \leftrightarrow (R \in CRing \to (\sum_{M} F \in U \leftrightarrow ran F \subseteq U)))$
30		eqid	$⊢ 1_{R} = 1_{R}$
31	3 30	ringidval	$⊢ 1_{R} = 0_{M}$
32	31	gsum0	$⊢ \sum_{M} \emptyset = 1_{R}$
33		crngring	$⊢ R \in CRing \to R \in Ring$
34	2 30	1unit	$⊢ R \in Ring \to 1_{R} \in U$
35	33 34	syl	$⊢ R \in CRing \to 1_{R} \in U$
36	32 35	eqeltrid	$⊢ R \in CRing \to \sum_{M} \emptyset \in U$
37		rn0	$⊢ ran \emptyset = \emptyset$
38		0ss	$⊢ \emptyset \subseteq U$
39	37 38	eqsstri	$⊢ ran \emptyset \subseteq U$
40	39	a1i	$⊢ R \in CRing \to ran \emptyset \subseteq U$
41	36 40	2thd	$⊢ R \in CRing \to (\sum_{M} \emptyset \in U \leftrightarrow ran \emptyset \subseteq U)$
42		simplr	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to R \in CRing$
43	3 1	mgpbas	$⊢ B = {Base}_{M}$
44	3	crngmgp	$⊢ R \in CRing \to M \in CMnd$
45	44	ad2antlr	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to M \in CMnd$
46		ovexd	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (0 ..^\|f\|) \in V$
47		wrdf	$⊢ f \in Word B \to f : (0 ..^\|f\|) ⟶ B$
48	47	ad3antrrr	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to f : (0 ..^\|f\|) ⟶ B$
49		fvexd	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to 1_{R} \in V$
50		simplll	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to f \in Word B$
51	49 50	wrdfsupp	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to {finSupp}_{1_{R}} (f)$
52	43 31 45 46 48 51	gsumcl	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to \sum_{M} f \in B$
53		simpllr	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to x \in B$
54		eqid	$⊢ \cdot_{R} = \cdot_{R}$
55	2 54 1	unitmulclb	$⊢ (R \in CRing \land \sum_{M} f \in B \land x \in B) \to ((\sum_{M}, f) \cdot_{R} x \in U \leftrightarrow (\sum_{M} f \in U \land x \in U))$
56	42 52 53 55	syl3anc	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to ((\sum_{M}, f) \cdot_{R} x \in U \leftrightarrow (\sum_{M} f \in U \land x \in U))$
57		simpr	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)$
58		vex	$⊢ x \in V$
59	58	snss	$⊢ x \in U \leftrightarrow \{x\} \subseteq U$
60		s1rn	$⊢ x \in B \to ran ⟨“ x ”⟩ = \{x\}$
61	60	sseq1d	$⊢ x \in B \to (ran ⟨“ x ”⟩ \subseteq U \leftrightarrow \{x\} \subseteq U)$
62	59 61	bitr4id	$⊢ x \in B \to (x \in U \leftrightarrow ran ⟨“ x ”⟩ \subseteq U)$
63	53 62	syl	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (x \in U \leftrightarrow ran ⟨“ x ”⟩ \subseteq U)$
64	57 63	anbi12d	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to ((\sum_{M} f \in U \land x \in U) \leftrightarrow (ran f \subseteq U \land ran ⟨“ x ”⟩ \subseteq U))$
65		unss	$⊢ (ran f \subseteq U \land ran ⟨“ x ”⟩ \subseteq U) \leftrightarrow ran f \cup ran ⟨“ x ”⟩ \subseteq U$
66	64 65	bitrdi	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to ((\sum_{M} f \in U \land x \in U) \leftrightarrow ran f \cup ran ⟨“ x ”⟩ \subseteq U)$
67	56 66	bitrd	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to ((\sum_{M}, f) \cdot_{R} x \in U \leftrightarrow ran f \cup ran ⟨“ x ”⟩ \subseteq U)$
68	3	ringmgp	$⊢ R \in Ring \to M \in Mnd$
69	33 68	syl	$⊢ R \in CRing \to M \in Mnd$
70	69	ad2antlr	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to M \in Mnd$
71	3 54	mgpplusg	$⊢ \cdot_{R} = +_{M}$
72	43 71	gsumccatsn	$⊢ (M \in Mnd \land f \in Word B \land x \in B) \to \sum_{M} (f ++ ⟨“ x ”⟩) = (\sum_{M}, f) \cdot_{R} x$
73	70 50 53 72	syl3anc	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to \sum_{M} (f ++ ⟨“ x ”⟩) = (\sum_{M}, f) \cdot_{R} x$
74	73	eleq1d	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (\sum_{M} (f ++ ⟨“ x ”⟩) \in U \leftrightarrow (\sum_{M}, f) \cdot_{R} x \in U)$
75	53	s1cld	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to ⟨“ x ”⟩ \in Word B$
76		ccatrn	$⊢ (f \in Word B \land ⟨“ x ”⟩ \in Word B) \to ran (f ++ ⟨“ x ”⟩) = ran f \cup ran ⟨“ x ”⟩$
77	50 75 76	syl2anc	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to ran (f ++ ⟨“ x ”⟩) = ran f \cup ran ⟨“ x ”⟩$
78	77	sseq1d	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (ran (f ++ ⟨“ x ”⟩) \subseteq U \leftrightarrow ran f \cup ran ⟨“ x ”⟩ \subseteq U)$
79	67 74 78	3bitr4d	$⊢ (((f \in Word B \land x \in B) \land R \in CRing) \land (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (\sum_{M} (f ++ ⟨“ x ”⟩) \in U \leftrightarrow ran (f ++ ⟨“ x ”⟩) \subseteq U)$
80	79	exp31	$⊢ (f \in Word B \land x \in B) \to (R \in CRing \to ((\sum_{M} f \in U \leftrightarrow ran f \subseteq U) \to (\sum_{M} (f ++ ⟨“ x ”⟩) \in U \leftrightarrow ran (f ++ ⟨“ x ”⟩) \subseteq U)))$
81	80	a2d	$⊢ (f \in Word B \land x \in B) \to ((R \in CRing \to (\sum_{M} f \in U \leftrightarrow ran f \subseteq U)) \to (R \in CRing \to (\sum_{M} (f ++ ⟨“ x ”⟩) \in U \leftrightarrow ran (f ++ ⟨“ x ”⟩) \subseteq U)))$
82	11 17 23 29 41 81	wrdind	$⊢ F \in Word B \to (R \in CRing \to (\sum_{M} F \in U \leftrightarrow ran F \subseteq U))$
83	5 4 82	sylc	$⊢ φ \to (\sum_{M} F \in U \leftrightarrow ran F \subseteq U)$

Metamath Proof Explorer

Theorem unitprodclb

Proof