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 5 9 mplringd 
 |-  ( ph -> P e. Ring )
30 ringsrg 
 |-  ( P e. Ring -> P e. SRing )
31 29 30 syl 
 |-  ( ph -> P e. SRing )
32 31 adantr 
 |-  ( ( ph /\ l e. S ) -> P e. SRing )
33 32 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> P e. SRing )
34 6 25 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
35 6 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
36 29 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 ffvelcdmda 
 |-  ( ( 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 34 7 37 45 49 mulgnn0cld 
 |-  ( ( ph /\ l e. S ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
51 50 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( Y ` l ) .^ ( V ` l ) ) e. ( Base ` P ) )
52 5 adantr 
 |-  ( ( ph /\ k e. S ) -> I e. W )
53 9 adantr 
 |-  ( ( ph /\ k e. S ) -> R e. Ring )
54 12 sselda 
 |-  ( ( ph /\ k e. S ) -> k e. I )
55 1 8 25 52 53 54 mvrcl 
 |-  ( ( ph /\ k e. S ) -> ( V ` k ) e. ( Base ` P ) )
56 55 adantlr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( V ` k ) e. ( Base ` P ) )
57 43 ffvelcdmda 
 |-  ( ( ph /\ k e. I ) -> ( Y ` k ) e. NN0 )
58 54 57 syldan 
 |-  ( ( ph /\ k e. S ) -> ( Y ` k ) e. NN0 )
59 58 adantlr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( Y ` k ) e. NN0 )
60 49 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( V ` l ) e. ( Base ` P ) )
61 45 adantr 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( Y ` l ) e. NN0 )
62 fveq2 
 |-  ( x = l -> ( V ` x ) = ( V ` l ) )
63 62 oveq2d 
 |-  ( x = l -> ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` y ) ( +g ` G ) ( V ` l ) ) )
64 62 oveq1d 
 |-  ( x = l -> ( ( V ` x ) ( +g ` G ) ( V ` y ) ) = ( ( V ` l ) ( +g ` G ) ( V ` y ) ) )
65 63 64 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 ) ) ) )
66 fveq2 
 |-  ( y = k -> ( V ` y ) = ( V ` k ) )
67 66 oveq1d 
 |-  ( y = k -> ( ( V ` y ) ( +g ` G ) ( V ` l ) ) = ( ( V ` k ) ( +g ` G ) ( V ` l ) ) )
68 66 oveq2d 
 |-  ( y = k -> ( ( V ` l ) ( +g ` G ) ( V ` y ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) )
69 67 68 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 ) ) ) )
70 65 69 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 ) ) ) )
71 48 54 anim12dan 
 |-  ( ( ph /\ ( l e. S /\ k e. S ) ) -> ( l e. I /\ k e. I ) )
72 70 71 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 ) ) ) )
73 72 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 ) ) ) ) )
74 11 73 mpcom 
 |-  ( ph -> ( ( l e. S /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) ) )
75 74 impl 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( V ` k ) ( +g ` G ) ( V ` l ) ) = ( ( V ` l ) ( +g ` G ) ( V ` k ) ) )
76 25 28 6 7 33 56 60 61 75 srgpcomp 
 |-  ( ( ( ph /\ l e. S ) /\ k e. S ) -> ( ( ( Y ` l ) .^ ( V ` l ) ) ( +g ` G ) ( V ` k ) ) = ( ( V ` k ) ( +g ` G ) ( ( Y ` l ) .^ ( V ` l ) ) ) )
77 25 28 6 7 33 51 56 59 76 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 ) ) ) )
78 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 ) ) ) )
79 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 ) ) ) )
80 79 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 ) ) ) )
81 78 80 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 ) ) ) ) )
82 77 81 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 ) ) )
83 82 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 ) ) ) )
84 83 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 ) ) ) )
85 84 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 ) ) ) )
86 85 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 ) ) ) )
87 24 86 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 ) ) ) )
88 19 87 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 ) ) ) )
89 88 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 ) ) ) )
90 16 89 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 ) ) ) )
91 90 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 ) )
92 91 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 ) )
93 eqid 
 |-  ( Base ` G ) = ( Base ` G )
94 36 adantr 
 |-  ( ( ph /\ k e. S ) -> G e. Mnd )
95 12 sseld 
 |-  ( ph -> ( k e. S -> k e. I ) )
96 95 imdistani 
 |-  ( ( ph /\ k e. S ) -> ( ph /\ k e. I ) )
97 96 57 syl 
 |-  ( ( ph /\ k e. S ) -> ( Y ` k ) e. NN0 )
98 55 34 eleqtrdi 
 |-  ( ( ph /\ k e. S ) -> ( V ` k ) e. ( Base ` G ) )
99 93 7 94 97 98 mulgnn0cld 
 |-  ( ( ph /\ k e. S ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` G ) )
100 99 fmpttd 
 |-  ( ph -> ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) : S --> ( Base ` G ) )
101 100 frnd 
 |-  ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( Base ` G ) )
102 eqid 
 |-  ( +g ` G ) = ( +g ` G )
103 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
104 93 102 103 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 ) ) )
105 101 101 104 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 ) ) )
106 92 105 mpbird 
 |-  ( ph -> ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. S |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )