Metamath Proof Explorer


Theorem vdwlem7

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem3.v φV
vdwlem3.w φW
vdwlem4.r φRFin
vdwlem4.h φH:1W2VR
vdwlem4.f F=x1Vy1WHy+Wx-1+V
vdwlem7.m φM
vdwlem7.g φG:1WR
vdwlem7.k φK2
vdwlem7.a φA
vdwlem7.d φD
vdwlem7.s φAAPKDF-1G
Assertion vdwlem7 φMKPolyAPGM+1KPolyAPHK+1MonoAPG

Proof

Step Hyp Ref Expression
1 vdwlem3.v φV
2 vdwlem3.w φW
3 vdwlem4.r φRFin
4 vdwlem4.h φH:1W2VR
5 vdwlem4.f F=x1Vy1WHy+Wx-1+V
6 vdwlem7.m φM
7 vdwlem7.g φG:1WR
8 vdwlem7.k φK2
9 vdwlem7.a φA
10 vdwlem7.d φD
11 vdwlem7.s φAAPKDF-1G
12 ovex 1WV
13 2nn0 20
14 eluznn0 20K2K0
15 13 8 14 sylancr φK0
16 eqid 1M=1M
17 12 15 7 6 16 vdwpc φMKPolyAPGad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=M
18 1 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MV
19 2 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MW
20 3 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MRFin
21 4 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MH:1W2VR
22 6 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MM
23 7 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MG:1WR
24 8 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MK2
25 9 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MA
26 10 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MD
27 11 ad2antrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MAAPKDF-1G
28 simplrl φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=Ma
29 simplrr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=Md1M
30 nnex V
31 ovex 1MV
32 30 31 elmap d1Md:1M
33 29 32 sylib φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=Md:1M
34 simprl φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=Mi1Ma+diAPKdiG-1Ga+di
35 fveq2 i=kdi=dk
36 35 oveq2d i=ka+di=a+dk
37 36 35 oveq12d i=ka+diAPKdi=a+dkAPKdk
38 36 fveq2d i=kGa+di=Ga+dk
39 38 sneqd i=kGa+di=Ga+dk
40 39 imaeq2d i=kG-1Ga+di=G-1Ga+dk
41 37 40 sseq12d i=ka+diAPKdiG-1Ga+dia+dkAPKdkG-1Ga+dk
42 41 cbvralvw i1Ma+diAPKdiG-1Ga+dik1Ma+dkAPKdkG-1Ga+dk
43 34 42 sylib φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=Mk1Ma+dkAPKdkG-1Ga+dk
44 38 cbvmptv i1MGa+di=k1MGa+dk
45 simprr φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=Mrani1MGa+di=M
46 eqid a+WA+VD-1=a+WA+VD-1
47 eqid j1M+1ifj=M+10dj+WD=j1M+1ifj=M+10dj+WD
48 18 19 20 21 5 22 23 24 25 26 27 28 33 43 44 45 46 47 vdwlem6 φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MM+1KPolyAPHK+1MonoAPG
49 48 ex φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MM+1KPolyAPHK+1MonoAPG
50 49 rexlimdvva φad1Mi1Ma+diAPKdiG-1Ga+dirani1MGa+di=MM+1KPolyAPHK+1MonoAPG
51 17 50 sylbid φMKPolyAPGM+1KPolyAPHK+1MonoAPG