Metamath Proof Explorer

Theorem unitscyglem1

Description: Lemma for unitscyg. (Contributed by metakunt, 13-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 
|- B = ( Base ` G )
unitscyglem1.2 
|- .^ = ( .g ` G )
unitscyglem1.3 
|- ( ph -> G e. Grp )
unitscyglem1.4 
|- ( ph -> B e. Fin )
unitscyglem1.5 
|- ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
unitscyglem1.6 
|- ( ph -> A e. B )
Assertion unitscyglem1 
|- ( ph -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) = ( ( od ` G ) ` A ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 
 |-  B = ( Base ` G )
2 unitscyglem1.2 
 |-  .^ = ( .g ` G )
3 unitscyglem1.3 
 |-  ( ph -> G e. Grp )
4 unitscyglem1.4 
 |-  ( ph -> B e. Fin )
5 unitscyglem1.5 
 |-  ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
6 unitscyglem1.6 
 |-  ( ph -> A e. B )
7 oveq1 
 |-  ( n = ( ( od ` G ) ` A ) -> ( n .^ x ) = ( ( ( od ` G ) ` A ) .^ x ) )
8 7 eqeq1d 
 |-  ( n = ( ( od ` G ) ` A ) -> ( ( n .^ x ) = ( 0g ` G ) <-> ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) ) )
9 8 rabbidv 
 |-  ( n = ( ( od ` G ) ` A ) -> { x e. B | ( n .^ x ) = ( 0g ` G ) } = { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
10 9 fveq2d 
 |-  ( n = ( ( od ` G ) ` A ) -> ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) = ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
11 id 
 |-  ( n = ( ( od ` G ) ` A ) -> n = ( ( od ` G ) ` A ) )
12 10 11 breq12d 
 |-  ( n = ( ( od ` G ) ` A ) -> ( ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n <-> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) <_ ( ( od ` G ) ` A ) ) )
13 eqid 
 |-  ( od ` G ) = ( od ` G )
14 1 13 odcl2 
 |-  ( ( G e. Grp /\ B e. Fin /\ A e. B ) -> ( ( od ` G ) ` A ) e. NN )
15 3 4 6 14 syl3anc 
 |-  ( ph -> ( ( od ` G ) ` A ) e. NN )
16 12 5 15 rspcdva 
 |-  ( ph -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) <_ ( ( od ` G ) ` A ) )
17 eqid 
 |-  ( i e. ZZ |-> ( i .^ A ) ) = ( i e. ZZ |-> ( i .^ A ) )
18 1 13 2 17 dfod2 
 |-  ( ( G e. Grp /\ A e. B ) -> ( ( od ` G ) ` A ) = if ( ran ( i e. ZZ |-> ( i .^ A ) ) e. Fin , ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) , 0 ) )
19 3 6 18 syl2anc 
 |-  ( ph -> ( ( od ` G ) ` A ) = if ( ran ( i e. ZZ |-> ( i .^ A ) ) e. Fin , ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) , 0 ) )
20 3 adantr 
 |-  ( ( ph /\ i e. ZZ ) -> G e. Grp )
21 simpr 
 |-  ( ( ph /\ i e. ZZ ) -> i e. ZZ )
22 6 adantr 
 |-  ( ( ph /\ i e. ZZ ) -> A e. B )
23 1 2 20 21 22 mulgcld 
 |-  ( ( ph /\ i e. ZZ ) -> ( i .^ A ) e. B )
24 23 fmpttd 
 |-  ( ph -> ( i e. ZZ |-> ( i .^ A ) ) : ZZ --> B )
25 frn 
 |-  ( ( i e. ZZ |-> ( i .^ A ) ) : ZZ --> B -> ran ( i e. ZZ |-> ( i .^ A ) ) C_ B )
26 24 25 syl 
 |-  ( ph -> ran ( i e. ZZ |-> ( i .^ A ) ) C_ B )
27 4 26 ssfid 
 |-  ( ph -> ran ( i e. ZZ |-> ( i .^ A ) ) e. Fin )
28 27 iftrued 
 |-  ( ph -> if ( ran ( i e. ZZ |-> ( i .^ A ) ) e. Fin , ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) , 0 ) = ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) )
29 19 28 eqtrd 
 |-  ( ph -> ( ( od ` G ) ` A ) = ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) )
30 eqid 
 |-  { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } = { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) }
31 fvexd 
 |-  ( ph -> ( Base ` G ) e. _V )
32 1 31 eqeltrid 
 |-  ( ph -> B e. _V )
33 30 32 rabexd 
 |-  ( ph -> { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } e. _V )
34 ovexd 
 |-  ( ( ph /\ i e. ZZ ) -> ( i .^ A ) e. _V )
35 34 fmpttd 
 |-  ( ph -> ( i e. ZZ |-> ( i .^ A ) ) : ZZ --> _V )
36 35 ffnd 
 |-  ( ph -> ( i e. ZZ |-> ( i .^ A ) ) Fn ZZ )
37 fvelrnb 
 |-  ( ( i e. ZZ |-> ( i .^ A ) ) Fn ZZ -> ( y e. ran ( i e. ZZ |-> ( i .^ A ) ) <-> E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) )
38 36 37 syl 
 |-  ( ph -> ( y e. ran ( i e. ZZ |-> ( i .^ A ) ) <-> E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) )
39 38 biimpa 
 |-  ( ( ph /\ y e. ran ( i e. ZZ |-> ( i .^ A ) ) ) -> E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y )
40 id 
 |-  ( ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y -> ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y )
41 40 eqcomd 
 |-  ( ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y -> y = ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) )
42 41 adantl 
 |-  ( ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) /\ ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y ) -> y = ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) )
43 simpll 
 |-  ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) -> ph )
44 simpr 
 |-  ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) -> w e. ZZ )
45 43 44 jca 
 |-  ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) -> ( ph /\ w e. ZZ ) )
46 eqidd 
 |-  ( ( ph /\ w e. ZZ ) -> ( i e. ZZ |-> ( i .^ A ) ) = ( i e. ZZ |-> ( i .^ A ) ) )
47 simpr 
 |-  ( ( ( ph /\ w e. ZZ ) /\ i = w ) -> i = w )
48 47 oveq1d 
 |-  ( ( ( ph /\ w e. ZZ ) /\ i = w ) -> ( i .^ A ) = ( w .^ A ) )
49 simpr 
 |-  ( ( ph /\ w e. ZZ ) -> w e. ZZ )
50 ovexd 
 |-  ( ( ph /\ w e. ZZ ) -> ( w .^ A ) e. _V )
51 46 48 49 50 fvmptd 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = ( w .^ A ) )
52 oveq2 
 |-  ( x = ( w .^ A ) -> ( ( ( od ` G ) ` A ) .^ x ) = ( ( ( od ` G ) ` A ) .^ ( w .^ A ) ) )
53 52 eqeq1d 
 |-  ( x = ( w .^ A ) -> ( ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) <-> ( ( ( od ` G ) ` A ) .^ ( w .^ A ) ) = ( 0g ` G ) ) )
54 3 adantr 
 |-  ( ( ph /\ w e. ZZ ) -> G e. Grp )
55 6 adantr 
 |-  ( ( ph /\ w e. ZZ ) -> A e. B )
56 1 2 54 49 55 mulgcld 
 |-  ( ( ph /\ w e. ZZ ) -> ( w .^ A ) e. B )
57 15 nnzd 
 |-  ( ph -> ( ( od ` G ) ` A ) e. ZZ )
58 57 adantr 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( od ` G ) ` A ) e. ZZ )
59 49 58 55 3jca 
 |-  ( ( ph /\ w e. ZZ ) -> ( w e. ZZ /\ ( ( od ` G ) ` A ) e. ZZ /\ A e. B ) )
60 1 2 mulgass 
 |-  ( ( G e. Grp /\ ( w e. ZZ /\ ( ( od ` G ) ` A ) e. ZZ /\ A e. B ) ) -> ( ( w x. ( ( od ` G ) ` A ) ) .^ A ) = ( w .^ ( ( ( od ` G ) ` A ) .^ A ) ) )
61 54 59 60 syl2anc 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( w x. ( ( od ` G ) ` A ) ) .^ A ) = ( w .^ ( ( ( od ` G ) ` A ) .^ A ) ) )
62 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
63 1 13 2 62 odid 
 |-  ( A e. B -> ( ( ( od ` G ) ` A ) .^ A ) = ( 0g ` G ) )
64 55 63 syl 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( ( od ` G ) ` A ) .^ A ) = ( 0g ` G ) )
65 64 oveq2d 
 |-  ( ( ph /\ w e. ZZ ) -> ( w .^ ( ( ( od ` G ) ` A ) .^ A ) ) = ( w .^ ( 0g ` G ) ) )
66 1 2 62 mulgz 
 |-  ( ( G e. Grp /\ w e. ZZ ) -> ( w .^ ( 0g ` G ) ) = ( 0g ` G ) )
67 3 66 sylan 
 |-  ( ( ph /\ w e. ZZ ) -> ( w .^ ( 0g ` G ) ) = ( 0g ` G ) )
68 65 67 eqtrd 
 |-  ( ( ph /\ w e. ZZ ) -> ( w .^ ( ( ( od ` G ) ` A ) .^ A ) ) = ( 0g ` G ) )
69 61 68 eqtr2d 
 |-  ( ( ph /\ w e. ZZ ) -> ( 0g ` G ) = ( ( w x. ( ( od ` G ) ` A ) ) .^ A ) )
70 59 simp2d 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( od ` G ) ` A ) e. ZZ )
71 70 49 55 3jca 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( ( od ` G ) ` A ) e. ZZ /\ w e. ZZ /\ A e. B ) )
72 1 2 mulgassr 
 |-  ( ( G e. Grp /\ ( ( ( od ` G ) ` A ) e. ZZ /\ w e. ZZ /\ A e. B ) ) -> ( ( w x. ( ( od ` G ) ` A ) ) .^ A ) = ( ( ( od ` G ) ` A ) .^ ( w .^ A ) ) )
73 54 71 72 syl2anc 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( w x. ( ( od ` G ) ` A ) ) .^ A ) = ( ( ( od ` G ) ` A ) .^ ( w .^ A ) ) )
74 69 73 eqtr2d 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( ( od ` G ) ` A ) .^ ( w .^ A ) ) = ( 0g ` G ) )
75 53 56 74 elrabd 
 |-  ( ( ph /\ w e. ZZ ) -> ( w .^ A ) e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
76 51 75 eqeltrd 
 |-  ( ( ph /\ w e. ZZ ) -> ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
77 45 76 syl 
 |-  ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) -> ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
78 77 adantr 
 |-  ( ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) /\ ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y ) -> ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
79 42 78 eqeltrd 
 |-  ( ( ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) /\ w e. ZZ ) /\ ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y ) -> y e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
80 nfv 
 |-  F/ w ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y
81 nfv 
 |-  F/ z ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y
82 fveqeq2 
 |-  ( z = w -> ( ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y <-> ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y ) )
83 80 81 82 cbvrexw 
 |-  ( E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y <-> E. w e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y )
84 83 biimpi 
 |-  ( E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y -> E. w e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y )
85 84 adantl 
 |-  ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) -> E. w e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` w ) = y )
86 79 85 r19.29a 
 |-  ( ( ph /\ E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y ) -> y e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
87 86 ex 
 |-  ( ph -> ( E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y -> y e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
88 87 adantr 
 |-  ( ( ph /\ y e. ran ( i e. ZZ |-> ( i .^ A ) ) ) -> ( E. z e. ZZ ( ( i e. ZZ |-> ( i .^ A ) ) ` z ) = y -> y e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
89 39 88 mpd 
 |-  ( ( ph /\ y e. ran ( i e. ZZ |-> ( i .^ A ) ) ) -> y e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
90 89 ex 
 |-  ( ph -> ( y e. ran ( i e. ZZ |-> ( i .^ A ) ) -> y e. { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
91 90 ssrdv 
 |-  ( ph -> ran ( i e. ZZ |-> ( i .^ A ) ) C_ { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
92 hashss 
 |-  ( ( { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } e. _V /\ ran ( i e. ZZ |-> ( i .^ A ) ) C_ { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) -> ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) <_ ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
93 33 91 92 syl2anc 
 |-  ( ph -> ( # ` ran ( i e. ZZ |-> ( i .^ A ) ) ) <_ ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
94 29 93 eqbrtrd 
 |-  ( ph -> ( ( od ` G ) ` A ) <_ ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
95 16 94 jca 
 |-  ( ph -> ( ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) <_ ( ( od ` G ) ` A ) /\ ( ( od ` G ) ` A ) <_ ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) ) )
96 ssrab2 
 |-  { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } C_ B
97 96 a1i 
 |-  ( ph -> { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } C_ B )
98 4 97 ssfid 
 |-  ( ph -> { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } e. Fin )
99 hashcl 
 |-  ( { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } e. Fin -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) e. NN0 )
100 98 99 syl 
 |-  ( ph -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) e. NN0 )
101 100 nn0red 
 |-  ( ph -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) e. RR )
102 15 nnred 
 |-  ( ph -> ( ( od ` G ) ` A ) e. RR )
103 101 102 letri3d 
 |-  ( ph -> ( ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) = ( ( od ` G ) ` A ) <-> ( ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) <_ ( ( od ` G ) ` A ) /\ ( ( od ` G ) ` A ) <_ ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) ) ) )
104 95 103 mpbird 
 |-  ( ph -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) = ( ( od ` G ) ` A ) )