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