Metamath Proof Explorer

Theorem idomsubgmo

Description: The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Hypothesis idomsubgmo.g 
|- G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
Assertion idomsubgmo 
|- ( ( R e. IDomn /\ N e. NN ) -> E* y e. ( SubGrp ` G ) ( # ` y ) = N )

Proof

Step Hyp Ref Expression
1 idomsubgmo.g 
 |-  G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
2 fvex 
 |-  ( Base ` G ) e. _V
3 2 rabex 
 |-  { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. _V
4 simp2l 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> y e. ( SubGrp ` G ) )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 subgss 
 |-  ( y e. ( SubGrp ` G ) -> y C_ ( Base ` G ) )
7 4 6 syl 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> y C_ ( Base ` G ) )
8 simpl2l 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. y ) -> y e. ( SubGrp ` G ) )
9 simp3l 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` y ) = N )
10 simp1r 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> N e. NN )
11 10 nnnn0d 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> N e. NN0 )
12 9 11 eqeltrd 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` y ) e. NN0 )
13 vex 
 |-  y e. _V
14 hashclb 
 |-  ( y e. _V -> ( y e. Fin <-> ( # ` y ) e. NN0 ) )
15 13 14 ax-mp 
 |-  ( y e. Fin <-> ( # ` y ) e. NN0 )
16 12 15 sylibr 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> y e. Fin )
17 16 adantr 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. y ) -> y e. Fin )
18 simpr 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. y ) -> z e. y )
19 eqid 
 |-  ( od ` G ) = ( od ` G )
20 19 odsubdvds 
 |-  ( ( y e. ( SubGrp ` G ) /\ y e. Fin /\ z e. y ) -> ( ( od ` G ) ` z ) || ( # ` y ) )
21 8 17 18 20 syl3anc 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. y ) -> ( ( od ` G ) ` z ) || ( # ` y ) )
22 9 adantr 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. y ) -> ( # ` y ) = N )
23 21 22 breqtrd 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. y ) -> ( ( od ` G ) ` z ) || N )
24 7 23 ssrabdv 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> y C_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } )
25 simp2r 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> x e. ( SubGrp ` G ) )
26 5 subgss 
 |-  ( x e. ( SubGrp ` G ) -> x C_ ( Base ` G ) )
27 25 26 syl 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> x C_ ( Base ` G ) )
28 simpl2r 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. x ) -> x e. ( SubGrp ` G ) )
29 simp3r 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` x ) = N )
30 29 11 eqeltrd 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` x ) e. NN0 )
31 vex 
 |-  x e. _V
32 hashclb 
 |-  ( x e. _V -> ( x e. Fin <-> ( # ` x ) e. NN0 ) )
33 31 32 ax-mp 
 |-  ( x e. Fin <-> ( # ` x ) e. NN0 )
34 30 33 sylibr 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> x e. Fin )
35 34 adantr 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. x ) -> x e. Fin )
36 simpr 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. x ) -> z e. x )
37 19 odsubdvds 
 |-  ( ( x e. ( SubGrp ` G ) /\ x e. Fin /\ z e. x ) -> ( ( od ` G ) ` z ) || ( # ` x ) )
38 28 35 36 37 syl3anc 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. x ) -> ( ( od ` G ) ` z ) || ( # ` x ) )
39 29 adantr 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. x ) -> ( # ` x ) = N )
40 38 39 breqtrd 
 |-  ( ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) /\ z e. x ) -> ( ( od ` G ) ` z ) || N )
41 27 40 ssrabdv 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> x C_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } )
42 24 41 unssd 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( y u. x ) C_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } )
43 ssdomg 
 |-  ( { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. _V -> ( ( y u. x ) C_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } -> ( y u. x ) ~<_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) )
44 3 42 43 mpsyl 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( y u. x ) ~<_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } )
45 1 5 19 idomodle 
 |-  ( ( R e. IDomn /\ N e. NN ) -> ( # ` { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) <_ N )
46 45 3ad2ant1 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) <_ N )
47 46 9 breqtrrd 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) <_ ( # ` y ) )
48 3 a1i 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. _V )
49 hashbnd 
 |-  ( ( { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. _V /\ ( # ` y ) e. NN0 /\ ( # ` { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) <_ ( # ` y ) ) -> { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. Fin )
50 48 12 47 49 syl3anc 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. Fin )
51 hashdom 
 |-  ( ( { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } e. Fin /\ y e. _V ) -> ( ( # ` { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) <_ ( # ` y ) <-> { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ~<_ y ) )
52 50 13 51 sylancl 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( ( # ` { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ) <_ ( # ` y ) <-> { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ~<_ y ) )
53 47 52 mpbid 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ~<_ y )
54 domtr 
 |-  ( ( ( y u. x ) ~<_ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } /\ { z e. ( Base ` G ) | ( ( od ` G ) ` z ) || N } ~<_ y ) -> ( y u. x ) ~<_ y )
55 44 53 54 syl2anc 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( y u. x ) ~<_ y )
56 13 31 unex 
 |-  ( y u. x ) e. _V
57 ssun1 
 |-  y C_ ( y u. x )
58 ssdomg 
 |-  ( ( y u. x ) e. _V -> ( y C_ ( y u. x ) -> y ~<_ ( y u. x ) ) )
59 56 57 58 mp2 
 |-  y ~<_ ( y u. x )
60 sbth 
 |-  ( ( ( y u. x ) ~<_ y /\ y ~<_ ( y u. x ) ) -> ( y u. x ) ~~ y )
61 55 59 60 sylancl 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( y u. x ) ~~ y )
62 9 29 eqtr4d 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( # ` y ) = ( # ` x ) )
63 hashen 
 |-  ( ( y e. Fin /\ x e. Fin ) -> ( ( # ` y ) = ( # ` x ) <-> y ~~ x ) )
64 16 34 63 syl2anc 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( ( # ` y ) = ( # ` x ) <-> y ~~ x ) )
65 62 64 mpbid 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> y ~~ x )
66 fiuneneq 
 |-  ( ( y ~~ x /\ y e. Fin ) -> ( ( y u. x ) ~~ y <-> y = x ) )
67 65 16 66 syl2anc 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> ( ( y u. x ) ~~ y <-> y = x ) )
68 61 67 mpbid 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) /\ ( ( # ` y ) = N /\ ( # ` x ) = N ) ) -> y = x )
69 68 3expia 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( y e. ( SubGrp ` G ) /\ x e. ( SubGrp ` G ) ) ) -> ( ( ( # ` y ) = N /\ ( # ` x ) = N ) -> y = x ) )
70 69 ralrimivva 
 |-  ( ( R e. IDomn /\ N e. NN ) -> A. y e. ( SubGrp ` G ) A. x e. ( SubGrp ` G ) ( ( ( # ` y ) = N /\ ( # ` x ) = N ) -> y = x ) )
71 fveqeq2 
 |-  ( y = x -> ( ( # ` y ) = N <-> ( # ` x ) = N ) )
72 71 rmo4 
 |-  ( E* y e. ( SubGrp ` G ) ( # ` y ) = N <-> A. y e. ( SubGrp ` G ) A. x e. ( SubGrp ` G ) ( ( ( # ` y ) = N /\ ( # ` x ) = N ) -> y = x ) )
73 70 72 sylibr 
 |-  ( ( R e. IDomn /\ N e. NN ) -> E* y e. ( SubGrp ` G ) ( # ` y ) = N )