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

Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
unitprodclb.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitprodclb.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
unitprodclb.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
unitprodclb.f ⊢ ( 𝜑 → 𝐹 ∈ Word 𝐵 )
Assertion unitprodclb ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) ∈ 𝑈 ↔ ran 𝐹 ⊆ 𝑈 ) )

Proof

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