Metamath Proof Explorer

Theorem mplcoe5lem

Description: Lemma for mplcoe4 . (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses mplcoe1.p 
|- P = ( I mPoly R )
mplcoe1.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplcoe1.z 
|- .0. = ( 0g ` R )
mplcoe1.o 
|- .1. = ( 1r ` R )
mplcoe1.i 
|- ( ph -> I e. W )
mplcoe2.g 
|- G = ( mulGrp ` P )
mplcoe2.m 
|- .^ = ( .g ` G )
mplcoe2.v 
|- V = ( I mVar R )
mplcoe5.r 
|- ( ph -> R e. Ring )
mplcoe5.y 
|- ( ph -> Y e. D )
mplcoe5.c 
|- ( ph -> A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
mplcoe5.s 
|- ( ph -> S C_ I )
Assertion mplcoe5lem 
|- ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p 
 |-  P = ( I mPoly R )
2 mplcoe1.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplcoe1.z 
 |-  .0. = ( 0g ` R )
4 mplcoe1.o 
 |-  .1. = ( 1r ` R )
5 mplcoe1.i 
 |-  ( ph -> I e. W )
6 mplcoe2.g 
 |-  G = ( mulGrp ` P )
7 mplcoe2.m 
 |-  .^ = ( .g ` G )
8 mplcoe2.v 
 |-  V = ( I mVar R )
9 mplcoe5.r 
 |-  ( ph -> R e. Ring )
10 mplcoe5.y 
 |-  ( ph -> Y e. D )
11 mplcoe5.c 
 |-  ( ph -> A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
12 mplcoe5.s 
 |-  ( ph -> S C_ I )
13 vex 
 |-  x e. _V
14 eqid 
 |-  ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) )
15 14 elrnmpt 
 |-  ( x e. _V -> ( x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) <-> E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) ) )
16 13 15 mp1i 
 |-  ( ph -> ( x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) <-> E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) ) )
17 vex 
 |-  y e. _V
18 14 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) <-> E. k e. S y = ( ( Y ` k ) .^ ( V ` k ) ) ) )
19 17 18 mp1i 
 |-  ( ph -> ( y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) <-> E. k e. S y = ( ( Y ` k ) .^ ( V ` k ) ) ) )
20 fveq2 
 |-  ( k = l -> ( Y ` k ) = ( Y ` l ) )
21 fveq2 
 |-  ( k = l -> ( V ` k ) = ( V ` l ) )
22 20 21 oveq12d 
 |-  ( k = l -> ( ( Y ` k ) .^ ( V ` k ) ) = ( ( Y ` l ) .^ ( V ` l ) ) )
23 22 eqeq2d 
 |-  ( k = l -> ( y = ( ( Y ` k ) .^ ( V ` k ) ) <-> y = ( ( Y ` l ) .^ ( V ` l ) ) ) )
24 23 cbvrexvw 
 |-  ( E. k e. S y = ( ( Y ` k ) .^ ( V ` k ) ) <-> E. l e. S y = ( ( Y ` l ) .^ ( V ` l ) ) )
25 eqid 
 |-  ( Base ` P ) = ( Base ` P )
26 eqid 
 |-  ( .r ` P ) = ( .r ` P )
27 6 26 mgpplusg 
 |-  ( .r ` P ) = ( +g ` G )
28 27 eqcomi 
 |-  ( +g ` G ) = ( .r ` P )
29 1 mplring 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. Ring )
30 5 9 29 syl2anc 
 |-  ( ph -> P e. Ring )
31 ringsrg 
 |-  ( P e. Ring -> P e. SRing )
32 30 31 syl 
 |-  ( ph -> P e. SRing )
33 32 adantr 
 |-  ( ( ph /\ l e. S ) -> P e. SRing )
34 33 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> P e. SRing )
35 6 25 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
36 6 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
37 30 36 syl 
 |-  ( ph -> G e. Mnd )
38 37 adantr 
 |-  ( ( ph /\ l e. S ) -> G e. Mnd )
39 12 sseld 
 |-  ( ph -> ( l e. S -> l e. I ) )
40 39 imdistani 
 |-  ( ( ph /\ l e. S ) -> ( ph /\ l e. I ) )
41 2 psrbag 
 |-  ( I e. W -> ( Y e. D <-> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) ) )
42 5 41 syl 
 |-  ( ph -> ( Y e. D <-> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) ) )
43 10 42 mpbid 
 |-  ( ph -> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) )
44 43 simpld 
 |-  ( ph -> Y : I --> NN0 )
45 44 ffvelcdmda 
 |-  ( ( ph /\ l e. I ) -> ( Y ` l ) e. NN0 )
46 40 45 syl 
 |-  ( ( ph /\ l e. S ) -> ( Y ` l ) e. NN0 )
47 5 adantr 
 |-  ( ( ph /\ l e. S ) -> I e. W )
48 9 adantr 
 |-  ( ( ph /\ l e. S ) -> R e. Ring )
49 12 sselda 
 |-  ( ( ph /\ l e. S ) -> l e. I )
50 1 8 25 47 48 49 mvrcl 
 |-  ( ( ph /\ l e. S ) -> ( V ` l ) e. ( Base ` P ) )
51 35 7 38 46 50 mulgnn0cld 
 |-  ( ( ph /\ l e. S ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
52 51 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
53 5 adantr 
 |-  ( ( ph /\ k e. S ) -> I e. W )
54 9 adantr 
 |-  ( ( ph /\ k e. S ) -> R e. Ring )
55 12 sselda 
 |-  ( ( ph /\ k e. S ) -> k e. I )
56 1 8 25 53 54 55 mvrcl 
 |-  ( ( ph /\ k e. S ) -> ( V ` k ) e. ( Base ` P ) )
57 56 adantlr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( V ` k ) e. ( Base ` P ) )
58 44 ffvelcdmda 
 |-  ( ( ph /\ k e. I ) -> ( Y ` k ) e. NN0 )
59 55 58 syldan 
 |-  ( ( ph /\ k e. S ) -> ( Y ` k ) e. NN0 )
60 59 adantlr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( Y ` k ) e. NN0 )
61 50 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( V ` l ) e. ( Base ` P ) )
62 46 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( Y ` l ) e. NN0 )
63 fveq2 
 |-  ( x = l -> ( V ` x ) = ( V ` l ) )
64 63 oveq2d 
 |-  ( x = l -> ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` y ) ( +g ` G ) ( V ` l ) ) )
65 63 oveq1d 
 |-  ( x = l -> ( ( V ` x ) ( +g ` G ) ( V ` y ) ) = ( ( V ` l ) ( +g ` G ) ( V ` y ) ) )
66 64 65 eqeq12d 
 |-  ( x = l -> ( ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) <-> ( ( V ` y ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` y ) ) ) )
67 fveq2 
 |-  ( y = k -> ( V ` y ) = ( V ` k ) )
68 67 oveq1d 
 |-  ( y = k -> ( ( V ` y ) ( +g ` G ) ( V ` l ) ) = ( ( V ` k ) ( +g ` G ) ( V ` l ) ) )
69 67 oveq2d 
 |-  ( y = k -> ( ( V ` l ) ( +g ` G ) ( V ` y ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) )
70 68 69 eqeq12d 
 |-  ( y = k -> ( ( ( V ` y ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` y ) ) <-> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) )
71 66 70 rspc2v 
 |-  ( ( l e. I /\ k e. I ) -> ( A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) )
72 49 55 anim12dan 
 |-  ( ( ph /\ ( l e. S /\ k e. S ) ) -> ( l e. I /\ k e. I ) )
73 71 72 syl11 
 |-  ( A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) -> ( ( ph /\ ( l e. S /\ k e. S ) ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) )
74 73 expd 
 |-  ( A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) -> ( ph -> ( ( l e. S /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) ) )
75 11 74 mpcom 
 |-  ( ph -> ( ( l e. S /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) )
76 75 impl 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) )
77 25 28 6 7 34 57 61 62 76 srgpcomp 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( V ` k ) ) = ( ( V ` k ) ( +g ` G ) ( ( Y ` l ) .^ ( V ` l ) ) ) )
78 25 28 6 7 34 52 57 60 77 srgpcomp 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( ( Y ` k ) .^ ( V ` k ) ) ( +g ` G ) ( ( Y ` l ) .^ ( V ` l ) ) ) = ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( ( Y ` k ) .^ ( V ` k ) ) ) )
79 oveq12 
 |-  ( ( x = ( ( Y ` k ) .^ ( V ` k ) ) /\ y = ( ( Y ` l ) .^ ( V ` l ) ) ) -> ( x ( +g ` G ) y ) = ( ( ( Y ` k ) .^ ( V ` k ) ) ( +g ` G ) ( ( Y ` l ) .^ ( V ` l ) ) ) )
80 oveq12 
 |-  ( ( y = ( ( Y ` l ) .^ ( V ` l ) ) /\ x = ( ( Y ` k ) .^ ( V ` k ) ) ) -> ( y ( +g ` G ) x ) = ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( ( Y ` k ) .^ ( V ` k ) ) ) )
81 80 ancoms 
 |-  ( ( x = ( ( Y ` k ) .^ ( V ` k ) ) /\ y = ( ( Y ` l ) .^ ( V ` l ) ) ) -> ( y ( +g ` G ) x ) = ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( ( Y ` k ) .^ ( V ` k ) ) ) )
82 79 81 eqeq12d 
 |-  ( ( x = ( ( Y ` k ) .^ ( V ` k ) ) /\ y = ( ( Y ` l ) .^ ( V ` l ) ) ) -> ( ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> ( ( ( Y ` k ) .^ ( V ` k ) ) ( +g ` G ) ( ( Y ` l ) .^ ( V ` l ) ) ) = ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
83 78 82 syl5ibrcom 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( x = ( ( Y ` k ) .^ ( V ` k ) ) /\ y = ( ( Y ` l ) .^ ( V ` l ) ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
84 83 expd 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( y = ( ( Y ` l ) .^ ( V ` l ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
85 84 rexlimdva 
 |-  ( ( ph /\ l e. S ) -> ( E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( y = ( ( Y ` l ) .^ ( V ` l ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
86 85 com23 
 |-  ( ( ph /\ l e. S ) -> ( y = ( ( Y ` l ) .^ ( V ` l ) ) -> ( E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
87 86 rexlimdva 
 |-  ( ph -> ( E. l e. S y = ( ( Y ` l ) .^ ( V ` l ) ) -> ( E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
88 24 87 biimtrid 
 |-  ( ph -> ( E. k e. S y = ( ( Y ` k ) .^ ( V ` k ) ) -> ( E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
89 19 88 sylbid 
 |-  ( ph -> ( y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) -> ( E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
90 89 com23 
 |-  ( ph -> ( E. k e. S x = ( ( Y ` k ) .^ ( V ` k ) ) -> ( y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
91 16 90 sylbid 
 |-  ( ph -> ( x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) -> ( y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) ) )
92 91 imp32 
 |-  ( ( ph /\ ( x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) /\ y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
93 92 ralrimivva 
 |-  ( ph -> A. x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) A. y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
94 eqid 
 |-  ( Base ` G ) = ( Base ` G )
95 37 adantr 
 |-  ( ( ph /\ k e. S ) -> G e. Mnd )
96 12 sseld 
 |-  ( ph -> ( k e. S -> k e. I ) )
97 96 imdistani 
 |-  ( ( ph /\ k e. S ) -> ( ph /\ k e. I ) )
98 97 58 syl 
 |-  ( ( ph /\ k e. S ) -> ( Y ` k ) e. NN0 )
99 56 35 eleqtrdi 
 |-  ( ( ph /\ k e. S ) -> ( V ` k ) e. ( Base ` G ) )
100 94 7 95 98 99 mulgnn0cld 
 |-  ( ( ph /\ k e. S ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` G ) )
101 100 fmpttd 
 |-  ( ph -> ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) : S --> ( Base ` G ) )
102 101 frnd 
 |-  ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( Base ` G ) )
103 eqid 
 |-  ( +g ` G ) = ( +g ` G )
104 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
105 94 103 104 sscntz 
 |-  ( ( ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( Base ` G ) /\ ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( Base ` G ) ) -> ( ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> A. x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) A. y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
106 102 102 105 syl2anc 
 |-  ( ph -> ( ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> A. x e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) A. y e. ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
107 93 106 mpbird 
 |-  ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )