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 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
36 30 35 syl 
 |-  ( ph -> G e. Mnd )
37 36 adantr 
 |-  ( ( ph /\ l e. S ) -> G e. Mnd )
38 12 sseld 
 |-  ( ph -> ( l e. S -> l e. I ) )
39 38 imdistani 
 |-  ( ( ph /\ l e. S ) -> ( ph /\ l e. I ) )
40 2 psrbag 
 |-  ( I e. W -> ( Y e. D <-> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) ) )
41 5 40 syl 
 |-  ( ph -> ( Y e. D <-> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) ) )
42 10 41 mpbid 
 |-  ( ph -> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) )
43 42 simpld 
 |-  ( ph -> Y : I --> NN0 )
44 43 ffvelrnda 
 |-  ( ( ph /\ l e. I ) -> ( Y ` l ) e. NN0 )
45 39 44 syl 
 |-  ( ( ph /\ l e. S ) -> ( Y ` l ) e. NN0 )
46 5 adantr 
 |-  ( ( ph /\ l e. S ) -> I e. W )
47 9 adantr 
 |-  ( ( ph /\ l e. S ) -> R e. Ring )
48 12 sselda 
 |-  ( ( ph /\ l e. S ) -> l e. I )
49 1 8 25 46 47 48 mvrcl 
 |-  ( ( ph /\ l e. S ) -> ( V ` l ) e. ( Base ` P ) )
50 6 25 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
51 50 7 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( Y ` l ) e. NN0 /\ ( V ` l ) e. ( Base ` P ) ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
52 37 45 49 51 syl3anc 
 |-  ( ( ph /\ l e. S ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
53 52 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
54 5 adantr 
 |-  ( ( ph /\ k e. S ) -> I e. W )
55 9 adantr 
 |-  ( ( ph /\ k e. S ) -> R e. Ring )
56 12 sselda 
 |-  ( ( ph /\ k e. S ) -> k e. I )
57 1 8 25 54 55 56 mvrcl 
 |-  ( ( ph /\ k e. S ) -> ( V ` k ) e. ( Base ` P ) )
58 57 adantlr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( V ` k ) e. ( Base ` P ) )
59 43 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( Y ` k ) e. NN0 )
60 56 59 syldan 
 |-  ( ( ph /\ k e. S ) -> ( Y ` k ) e. NN0 )
61 60 adantlr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( Y ` k ) e. NN0 )
62 49 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( V ` l ) e. ( Base ` P ) )
63 45 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( Y ` l ) e. NN0 )
64 fveq2 
 |-  ( x = l -> ( V ` x ) = ( V ` l ) )
65 64 oveq2d 
 |-  ( x = l -> ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` y ) ( +g ` G ) ( V ` l ) ) )
66 64 oveq1d 
 |-  ( x = l -> ( ( V ` x ) ( +g ` G ) ( V ` y ) ) = ( ( V ` l ) ( +g ` G ) ( V ` y ) ) )
67 65 66 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 ) ) ) )
68 fveq2 
 |-  ( y = k -> ( V ` y ) = ( V ` k ) )
69 68 oveq1d 
 |-  ( y = k -> ( ( V ` y ) ( +g ` G ) ( V ` l ) ) = ( ( V ` k ) ( +g ` G ) ( V ` l ) ) )
70 68 oveq2d 
 |-  ( y = k -> ( ( V ` l ) ( +g ` G ) ( V ` y ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) )
71 69 70 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 ) ) ) )
72 67 71 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 ) ) ) )
73 48 56 anim12dan 
 |-  ( ( ph /\ ( l e. S /\ k e. S ) ) -> ( l e. I /\ k e. I ) )
74 72 73 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 ) ) ) )
75 74 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 ) ) ) ) )
76 11 75 mpcom 
 |-  ( ph -> ( ( l e. S /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) )
77 76 impl 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) )
78 25 28 6 7 34 58 62 63 77 srgpcomp 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( V ` k ) ) = ( ( V ` k ) ( +g ` G ) ( ( Y ` l ) .^ ( V ` l ) ) ) )
79 25 28 6 7 34 53 58 61 78 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 ) ) ) )
80 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 ) ) ) )
81 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 ) ) ) )
82 81 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 ) ) ) )
83 80 82 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 ) ) ) ) )
84 79 83 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 ) ) )
85 84 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 ) ) ) )
86 85 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 ) ) ) )
87 86 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 ) ) ) )
88 87 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 ) ) ) )
89 24 88 syl5bi 
 |-  ( 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 ) ) ) )
90 19 89 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 ) ) ) )
91 90 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 ) ) ) )
92 16 91 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 ) ) ) )
93 92 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 ) )
94 93 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 ) )
95 36 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 59 syl 
 |-  ( ( ph /\ k e. S ) -> ( Y ` k ) e. NN0 )
99 57 50 eleqtrdi 
 |-  ( ( ph /\ k e. S ) -> ( V ` k ) e. ( Base ` G ) )
100 eqid 
 |-  ( Base ` G ) = ( Base ` G )
101 100 7 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( Y ` k ) e. NN0 /\ ( V ` k ) e. ( Base ` G ) ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` G ) )
102 95 98 99 101 syl3anc 
 |-  ( ( ph /\ k e. S ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` G ) )
103 102 fmpttd 
 |-  ( ph -> ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) : S --> ( Base ` G ) )
104 103 frnd 
 |-  ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( Base ` G ) )
105 eqid 
 |-  ( +g ` G ) = ( +g ` G )
106 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
107 100 105 106 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 ) ) )
108 104 104 107 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 ) ) )
109 94 108 mpbird 
 |-  ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )